---

Step * 1 1 3 of Lemma rng_to_alg_wf

.....wf..... 
1. R : Rng
2. Comm(|R|;*)
3. m : algebra_sig{i:l}(|R|)
⊢ IsGroup(m.car;m.plus;m.zero;m.minus)
  ∧ Comm(m.car;m.plus)
  ∧ IsAction(|R|;*;1;m.car;m.act)
  ∧ IsBilinear(|R|;m.car;m.car;+R;m.plus;m.plus;m.act) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  R  :  Rng
2.  Comm(|R|;*)
3.  m  :  algebra\_sig\{i:l\}(|R|)
\mvdash{}  IsGroup(m.car;m.plus;m.zero;m.minus)
    \mwedge{}  Comm(m.car;m.plus)
    \mwedge{}  IsAction(|R|;*;1;m.car;m.act)
    \mwedge{}  IsBilinear(|R|;m.car;m.car;+R;m.plus;m.plus;m.act)  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index