---

Step * 1 3 of Lemma rng_to_alg_wf

.....wf..... 
1. R : Rng
2. Comm(|R|;*)
3. m : R-Module
⊢ IsMonoid(m.car;m.times;m.one) ∧ BiLinear(m.car;m.plus;m.times) ∧ (∀a:|R|. Dist1op2opLR(m.car;m.act a;m.times)) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  R  :  Rng
2.  Comm(|R|;*)
3.  m  :  R-Module
\mvdash{}  IsMonoid(m.car;m.times;m.one)
    \mwedge{}  BiLinear(m.car;m.plus;m.times)
    \mwedge{}  (\mforall{}a:|R|.  Dist1op2opLR(m.car;m.act  a;m.times))  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index