---

Step * 1 1 1 of Lemma int_ring_wf


ℤ-rng ∈ RngSig
BY
{ AbEval ``int_ring rng_sig`` 0  }

1
<ℤ, λu,v. (u =z v), λu,v. u ≤z v, λu,v. (u + v), 0, λu.(-u), λu,v. (u * v), 1, λu,v. if (v =z 0) then inr ⋅  else inl (u\000C ÷ v) fi >
∈ car:Type
× eq:car ⟶ car ⟶ 𝔹
× le:car ⟶ car ⟶ 𝔹
× plus:car ⟶ car ⟶ car
× zero:car
× minus:car ⟶ car
× times:car ⟶ car ⟶ car
× one:car
× (car ⟶ car ⟶ (car?))

---

Latex:

---

Latex:

\mBbbZ{}-rng  \mmember{}  RngSig


By

---

Latex:
AbEval  ``int\_ring  rng\_sig``  0 

---

Home Index