---

Step * of Lemma module_act_minus_l

∀A:Rng. ∀m:A-Module. ∀a:|A|. ∀u:m.car.  (((-A a) m.act 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 a) m.act 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  a)  m.act  u)  =  (m.minus  (a  m.act  u)))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index