---

Step * of Lemma alg_div_wf

∀A:Type. ∀a:algebra_sig{i:l}(A).  (a.div ∈ a.car ⟶ a.car ⟶ (a.car?))
BY
{ ModulePiTac 10 ``alg_car alg_eq alg_le alg_plus alg_zero alg_minus alg_times alg_one alg_div alg_act`` }

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}a:algebra\_sig\{i:l\}(A).    (a.div  \mmember{}  a.car  {}\mrightarrow{}  a.car  {}\mrightarrow{}  (a.car?))


By

---

Latex:
...

---

Home Index