---

Step * of Lemma ring_p_wf

∀[T:Type]. ∀[pl:T ⟶ T ⟶ T]. ∀[zero:T]. ∀[neg:T ⟶ T]. ∀[tm:T ⟶ T ⟶ T]. ∀[one:T].  (IsRing(T;pl;zero;neg;tm;one) ∈ ℙ)
BY
{ Unfold `ring_p` 0 THEN Auto⋅ }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[pl:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[zero:T].  \mforall{}[neg:T  {}\mrightarrow{}  T].  \mforall{}[tm:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[one:T].
    (IsRing(T;pl;zero;neg;tm;one)  \mmember{}  \mBbbP{})


By

---

Latex:
Unfold  `ring\_p`  0  THEN  Auto\mcdot{}

---

Home Index