---

Step * 1 1 1 1 of Lemma rng_to_alg_wf


1. R : RngSig
2. IsRing(|R|;+R;0;-R;*;1)
3. Comm(|R|;*)
⊢ rng_to_alg(R) ∈ algebra_sig{i:l}(|R|)
BY
{ Unfolds ``rng_to_alg algebra_sig`` 0 }

1
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)

---

Latex:

---

Latex:

1.  R  :  RngSig
2.  IsRing(|R|;+R;0;-R;*;1)
3.  Comm(|R|;*)
\mvdash{}  rng\_to\_alg(R)  \mmember{}  algebra\_sig\{i:l\}(|R|)


By

---

Latex:
Unfolds  ``rng\_to\_alg  algebra\_sig``  0

---

Home Index