---

Step * of Lemma module_act_minus_r

∀A:Rng. ∀m:A-Module. ∀a:|A|. ∀u:m.car.  ((a m.act (m.minus u)) = (m.minus (a m.act u)) ∈ m.car)
BY
{ ((RepD) THENA Auto) }

1
1. A : Rng
2. m : A-Module
3. a : |A|
4. u : m.car
⊢ (a m.act (m.minus u)) = (m.minus (a m.act u)) ∈ m.car

---

Latex:

---

Latex:
\mforall{}A:Rng.  \mforall{}m:A-Module.  \mforall{}a:|A|.  \mforall{}u:m.car.    ((a  m.act  (m.minus  u))  =  (m.minus  (a  m.act  u)))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index