---

Step * 2 of Lemma module_act_grp_hom_l


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index