---

Step * 2 of Lemma module_act_is_grp_hom


1. A : Rng@i'
2. m : A-Module@i'
3. a : |A|@i
⊢ (m.act a m.zero) = m.zero ∈ m.car
BY
{ ((BLemma `module_act_zero_r`) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Rng@i'
2.  m  :  A-Module@i'
3.  a  :  |A|@i
\mvdash{}  (m.act  a  m.zero)  =  m.zero


By

---

Latex:
((BLemma  `module\_act\_zero\_r`)  THEN  Auto)

---

Home Index