---

Step * 1 1 1 1 1 of Lemma rng_to_alg_wf


1. R : RngSig
2. IsRing(|R|;+R;0;-R;*;1)
3. Comm(|R|;*)
⊢ <|R|, =b, ≤b, +R, 0, -R, *, 1, ÷R, *> ∈ car:Type
  × eq:car ⟶ car ⟶ 𝔹
  × le:car ⟶ car ⟶ 𝔹
  × plus:car ⟶ car ⟶ car
  × zero:car
  × minus:car ⟶ car
  × times:car ⟶ car ⟶ car
  × one:car
  × div:car ⟶ car ⟶ (car?)
  × (|R| ⟶ car ⟶ car)
BY
{ Auto }

---

Latex:

---

Latex:

1.  R  :  RngSig
2.  IsRing(|R|;+R;0;-R;*;1)
3.  Comm(|R|;*)
\mvdash{}  <|R|,  =\msubb{},  \mleq{}\msubb{},  +R,  0,  -R,  *,  1,  \mdiv{}R,  *>  \mmember{}  car:Type
    \mtimes{}  eq:car  {}\mrightarrow{}  car  {}\mrightarrow{}  \mBbbB{}
    \mtimes{}  le:car  {}\mrightarrow{}  car  {}\mrightarrow{}  \mBbbB{}
    \mtimes{}  plus:car  {}\mrightarrow{}  car  {}\mrightarrow{}  car
    \mtimes{}  zero:car
    \mtimes{}  minus:car  {}\mrightarrow{}  car
    \mtimes{}  times:car  {}\mrightarrow{}  car  {}\mrightarrow{}  car
    \mtimes{}  one:car
    \mtimes{}  div:car  {}\mrightarrow{}  car  {}\mrightarrow{}  (car?)
    \mtimes{}  (|R|  {}\mrightarrow{}  car  {}\mrightarrow{}  car)


By

---

Latex:
Auto

---

Home Index