---

Step * of Lemma module_over_triv_rng

∀A:Rng. ∀m:A-Module.  ((1 = 0 ∈ |A|) ⇒ (∀u:m.car. (u = m.zero ∈ m.car)))
BY
{ ((RepD) THENA Auto) }

1
1. A : Rng
2. m : A-Module
3. 1 = 0 ∈ |A|
4. u : m.car
⊢ u = m.zero ∈ m.car

---

Latex:

---

Latex:
\mforall{}A:Rng.  \mforall{}m:A-Module.    ((1  =  0)  {}\mRightarrow{}  (\mforall{}u:m.car.  (u  =  m.zero)))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index