---

Step * 1 1 1 of Lemma int_mod_ring_wf


1. n : ℕ+
⊢ <ℤ_n, λu,v. (u mod n =z v mod n), λu,v. ff, λu,v. (u + v), 0, λu.(-u), λu,v. (u * v), 1, λu,v. (inr ⋅ )> ∈ Rng
BY
{ (MemTypeCD THEN Reduce 0) }

1
1. n : ℕ+
⊢ <ℤ_n, λu,v. (u mod n =z v mod n), λu,v. ff, λu,v. (u + v), 0, λu.(-u), λu,v. (u * v), 1, λu,v. (inr ⋅ )> ∈ RngSig

2
1. n : ℕ+
⊢ IsRing(ℤ_n;λu,v. (u + v);0;λu.(-u);λu,v. (u * v);1)

3
.....wf..... 
1. n : ℕ+
2. r : RngSig
⊢ istype(IsRing(|r|;+r;0;-r;*;1))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  <\mBbbZ{}\_n,  \mlambda{}u,v.  (u  mod  n  =\msubz{}  v  mod  n),  \mlambda{}u,v.  ff,  \mlambda{}u,v.  (u  +  v),  0,  \mlambda{}u.(-u),  \mlambda{}u,v.  (u  *  v),  1,  \mlambda{}u,v.  (in\000Cr  \mcdot{}  )>  \mmember{}  Rng


By

---

Latex:
(MemTypeCD  THEN  Reduce  0)

---

Home Index