---

Step * of Lemma module_properties

∀A:RngSig. ∀m:A-Module.
  (IsGroup(m.car;m.plus;m.zero;m.minus)
  ∧ Comm(m.car;m.plus)
  ∧ IsAction(|A|;*;1;m.car;m.act)
  ∧ IsBilinear(|A|;m.car;m.car;+A;m.plus;m.plus;m.act))
BY
{ (Auto THEN D 2 THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A:RngSig.  \mforall{}m:A-Module.
    (IsGroup(m.car;m.plus;m.zero;m.minus)
    \mwedge{}  Comm(m.car;m.plus)
    \mwedge{}  IsAction(|A|;*;1;m.car;m.act)
    \mwedge{}  IsBilinear(|A|;m.car;m.car;+A;m.plus;m.plus;m.act))


By

---

Latex:
(Auto  THEN  D  2  THEN  Unhide  THEN  Auto)

---

Home Index