---

Step * 3 of Lemma alg_act_is_rng_chom


1. a : CRng
2. m : algebra{i:l}(a)
⊢ (m.act 1 m.one) = m.one ∈ m.car
BY
{ ((RWW "module_action_p.2" 0) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  CRng
2.  m  :  algebra\{i:l\}(a)
\mvdash{}  (m.act  1  m.one)  =  m.one


By

---

Latex:
((RWW  "module\_action\_p.2"  0)  THEN  Auto)

---

Home Index