Definition: rng_sig
`RngSig ==`
`  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?))`

Lemma: rng_sig_wf
`RngSig ∈ 𝕌'`

Definition: rng_car
`|r| ==  fst(r)`

Lemma: rng_car_wf
`∀[r:RngSig]. (|r| ∈ Type)`

Definition: rng_eq
`=b ==  fst(snd(r))`

Lemma: rng_eq_wf
`∀[r:RngSig]. (=b ∈ |r| ⟶ |r| ⟶ 𝔹)`

Definition: rng_le
`≤b ==  fst(snd(snd(r)))`

Lemma: rng_le_wf
`∀[r:RngSig]. (≤b ∈ |r| ⟶ |r| ⟶ 𝔹)`

Definition: rng_plus
`+r ==  fst(snd(snd(snd(r))))`

Lemma: rng_plus_wf
`∀[r:RngSig]. (+r ∈ |r| ⟶ |r| ⟶ |r|)`

Definition: rng_zero
`0 ==  fst(snd(snd(snd(snd(r)))))`

Lemma: rng_zero_wf
`∀[r:RngSig]. (0 ∈ |r|)`

Definition: rng_minus
`-r ==  fst(snd(snd(snd(snd(snd(r))))))`

Lemma: rng_minus_wf
`∀[r:RngSig]. (-r ∈ |r| ⟶ |r|)`

Definition: rng_times
`* ==  fst(snd(snd(snd(snd(snd(snd(r)))))))`

Lemma: rng_times_wf
`∀[r:RngSig]. (* ∈ |r| ⟶ |r| ⟶ |r|)`

Definition: rng_one
`1 ==  fst(snd(snd(snd(snd(snd(snd(snd(r))))))))`

Lemma: rng_one_wf
`∀[r:RngSig]. (1 ∈ |r|)`

Definition: rng_div
`÷r ==  snd(snd(snd(snd(snd(snd(snd(snd(r))))))))`

Lemma: rng_div_wf
`∀[r:RngSig]. (÷r ∈ |r| ⟶ |r| ⟶ (|r|?))`

Lemma: subtype_rel_rng_sig
`RngSig ⊆r RngSig{[i | j]}`

Lemma: rng_sig_inc
`RngSig ⊆r RngSig{[i | j]}`

Definition: ring_p
`IsRing(T;plus;zero;neg;times;one) ==  IsGroup(T;plus;zero;neg) ∧ IsMonoid(T;times;one) ∧ BiLinear(T;plus;times)`

Lemma: ring_p_wf
`∀[T:Type]. ∀[pl:T ⟶ T ⟶ T]. ∀[zero:T]. ∀[neg:T ⟶ T]. ∀[tm:T ⟶ T ⟶ T]. ∀[one:T].  (IsRing(T;pl;zero;neg;tm;one) ∈ ℙ)`

Definition: rng
`Rng ==  {r:RngSig| IsRing(|r|;+r;0;-r;*;1)} `

Definition: drng
`DRng ==  {r:RngSig| IsRing(|r|;+r;0;-r;*;1) ∧ IsEqFun(|r|;=b)} `

Lemma: rng_wf
`Rng ∈ 𝕌'`

Lemma: rng_subtype_rng_sig
`Rng ⊆r RngSig`

Lemma: drng_wf
`DRng ∈ 𝕌'`

Lemma: drng_subtype_rng
`DRng ⊆r Rng`

Lemma: rng_properties
`∀[r:Rng]. IsRing(|r|;+r;0;-r;*;1)`

Lemma: drng_properties
`∀[r:DRng]. (IsRing(|r|;+r;0;-r;*;1) ∧ IsEqFun(|r|;=b))`

Lemma: rng_all_properties
`∀[r:Rng]. (Assoc(|r|;+r) ∧ Ident(|r|;+r;0) ∧ Inverse(|r|;+r;0;-r) ∧ Assoc(|r|;*) ∧ Ident(|r|;*;1) ∧ BiLinear(|r|;+r;*))`

Lemma: drng_all_properties
`∀[r:DRng]`
`  (Assoc(|r|;+r)`
`  ∧ Ident(|r|;+r;0)`
`  ∧ Inverse(|r|;+r;0;-r)`
`  ∧ Assoc(|r|;*)`
`  ∧ Ident(|r|;*;1)`
`  ∧ BiLinear(|r|;+r;*)`
`  ∧ IsEqFun(|r|;=b))`

Lemma: assert_of_rng_eq
`∀[r:DRng]. ∀[a,b:|r|].  uiff(↑(a =b b);a = b ∈ |r|)`

Lemma: decidable__rng_eq
`∀r:DRng. ∀u,v:|r|.  Dec(u = v ∈ |r|)`

Definition: crng
`CRng ==  {r:Rng| Comm(|r|;*)} `

Definition: cdrng
`CDRng ==  {r:CRng| IsEqFun(|r|;=b)} `

Lemma: crng_wf
`CRng ∈ 𝕌'`

Lemma: crng_subtype_rng
`CRng ⊆r Rng`

Lemma: cdrng_wf
`CDRng ∈ 𝕌'`

Lemma: cdrng_subtype_crng
`CDRng ⊆r CRng`

Lemma: cdrng_subtype_drng
`CDRng ⊆r DRng`

Lemma: crng_properties
`∀[r:CRng]. Comm(|r|;*)`

Lemma: cdrng_properties
`∀[r:CDRng]. IsEqFun(|r|;=b)`

Lemma: crng_all_properties
`∀[r:CRng]`
`  (Assoc(|r|;+r)`
`  ∧ Ident(|r|;+r;0)`
`  ∧ Inverse(|r|;+r;0;-r)`
`  ∧ Assoc(|r|;*)`
`  ∧ Comm(|r|;*)`
`  ∧ Ident(|r|;*;1)`
`  ∧ BiLinear(|r|;+r;*))`

Definition: mul_mon_of_rng
`r↓xmn ==  <|r|, =b, ≤b, *, 1, λz.z>`

Lemma: mul_mon_of_rng_wf
`∀[r:RngSig]. (r↓xmn ∈ GrpSig)`

Lemma: mul_mon_of_rng_wf_c
`∀[r:Rng]. (r↓xmn ∈ IMonoid)`

Lemma: mul_mon_of_rng_wf_a
`∀[r:Rng]. (r↓xmn ∈ Mon)`

Lemma: mul_mon_of_rng_wf_b
`∀[r:CRng]. (r↓xmn ∈ AbMon)`

`r↓+gp ==  <|r|, =b, ≤b, +r, 0, -r>`

`∀[r:RngSig]. (r↓+gp ∈ GrpSig)`

`∀[r:Rng]. (r↓+gp ∈ Group{i})`

Lemma: rng_minus_over_plus
`∀[r:Rng]. ∀[a,b:|r|].  ((-r (a +r b)) = ((-r b) +r (-r a)) ∈ |r|)`

Lemma: rng_minus_minus
`∀[r:Rng]. ∀[a:|r|].  ((-r (-r a)) = a ∈ |r|)`

Lemma: rng_minus_zero
`∀[r:Rng]. ((-r 0) = 0 ∈ |r|)`

Lemma: rng_plus_inv
`∀[r:Rng]. ∀[a:|r|].  (((a +r (-r a)) = 0 ∈ |r|) ∧ (((-r a) +r a) = 0 ∈ |r|))`

Lemma: rng_plus_inv_assoc
`∀[r:Rng]. ∀[a,b:|r|].  (((a +r ((-r a) +r b)) = b ∈ |r|) ∧ (((-r a) +r (a +r b)) = b ∈ |r|))`

Lemma: rng_plus_zero
`∀[r:Rng]. ∀[a:|r|].  (((a +r 0) = a ∈ |r|) ∧ ((0 +r a) = a ∈ |r|))`

Lemma: rng_plus_cancel_l
`∀[r:Rng]. ∀[a,b,c:|r|].  b = c ∈ |r| supposing (a +r b) = (a +r c) ∈ |r|`

Lemma: rng_plus_assoc
`∀[r:Rng]. ∀[a,b,c:|r|].  ((a +r (b +r c)) = ((a +r b) +r c) ∈ |r|)`

Lemma: rng_times_assoc
`∀[r:Rng]. ∀[a,b,c:|r|].  ((a * (b * c)) = ((a * b) * c) ∈ |r|)`

Lemma: rng_times_one
`∀[r:Rng]. ∀[a:|r|].  (((a * 1) = a ∈ |r|) ∧ ((1 * a) = a ∈ |r|))`

Lemma: crng_times_comm
`∀[r:CRng]. ∀[a,b:|r|].  ((a * b) = (b * a) ∈ |r|)`

Lemma: crng_times_ac_1
`∀[r:CRng]. ∀[a,b,c:|r|].  ((a * (b * c)) = (b * (a * c)) ∈ |r|)`

Lemma: rng_times_over_plus
`∀[r:Rng]. ∀[a,b,c:|r|].  (((a * (b +r c)) = ((a * b) +r (a * c)) ∈ |r|) ∧ (((b +r c) * a) = ((b * a) +r (c * a)) ∈ |r|))`

Lemma: rng_times_zero
`∀[r:Rng]. ∀[a:|r|].  (((0 * a) = 0 ∈ |r|) ∧ ((a * 0) = 0 ∈ |r|))`

Lemma: rng_times_over_minus
`∀[r:Rng]. ∀[a,b:|r|].  ((((-r a) * b) = (-r (a * b)) ∈ |r|) ∧ ((a * (-r b)) = (-r (a * b)) ∈ |r|))`

Lemma: rng_plus_comm
`∀[r:Rng]. ∀[a,b:|r|].  ((a +r b) = (b +r a) ∈ |r|)`

Lemma: rng_plus_comm2
`∀[r:Rng]. Comm(|r|;+r)`

`∀[r:Rng]. (r↓+gp ∈ AbGrp)`

Lemma: rng_plus_ac_1
`∀[r:Rng]. ∀[a,b,c:|r|].  ((a +r (b +r c)) = (b +r (a +r c)) ∈ |r|)`

Lemma: ring_triv
`∀[r:Rng]. ∀[a:|r|]. (a = 0 ∈ |r|) supposing 1 = 0 ∈ |r|`

Definition: rng_sum
`Σ(r) i ≤ k < j. E[k] ==  Π i ≤ k < j. E[k]`

Lemma: rng_sum_wf
`∀[r:Rng]. ∀[p,q:ℤ]. ∀[E:{p..q-} ⟶ |r|].  (Σ(r) p ≤ i < q. E[i] ∈ |r|)`

Lemma: comb_for_rng_sum_wf
`λr,p,q,E,z. (Σ(r) p ≤ i < q. E[i]) ∈ r:Rng ⟶ p:ℤ ⟶ q:ℤ ⟶ E:({p..q-} ⟶ |r|) ⟶ (↓True) ⟶ |r|`

Definition: rng_prod
`Π(r) i ≤ k < j. E[k] ==  Π i ≤ k < j. E[k]`

Lemma: rng_prod_wf
`∀[r:Rng]. ∀[p,q:ℤ]. ∀[E:{p..q-} ⟶ |r|].  (Π(r) p ≤ i < q. E[i] ∈ |r|)`

Lemma: cdrng_is_abdmonoid
`∀[r:CDRng]. ((r↓+gp ∈ AbDMon) ∧ (r↓xmn ∈ AbDMon))`

Lemma: cdrng_is_abdgrp
`∀[r:CDRng]. (r↓+gp ∈ AbDGrp)`

Definition: ring_divs
`a | b in r ==  ∃c:|r|. ((c * a) = b ∈ |r|)`

Lemma: ring_divs_wf
`∀[r:RngSig]. ∀[p,q:|r|].  (p | q in r ∈ ℙ)`

Definition: ring_non_triv
`r ≠ 0 ==  1 ≠ 0 ∈ |r| `

Lemma: ring_non_triv_wf
`∀[r:Rng]. (r ≠ 0 ∈ ℙ)`

Definition: integ_dom_p
`IsIntegDom(r) ==  0 ≠ 1 ∈ |r|  ∧ (∀u,v:|r|.  ((¬(v = 0 ∈ |r|)) `` ((u * v) = 0 ∈ |r|) `` (u = 0 ∈ |r|)))`

Lemma: integ_dom_p_wf
`∀[r:CRng]. (IsIntegDom(r) ∈ ℙ)`

Lemma: sq_stable__integ_dom_p
`∀[r:CRng]. SqStable(IsIntegDom(r))`

Definition: field_p
`IsField(r) ==  0 ≠ 1 ∈ |r|  ∧ (∀u:|r|. (u ≠ 0 ∈ |r|  `` u | 1 in r))`

Lemma: field_p_wf
`∀[r:RngSig]. (IsField(r) ∈ ℙ)`

Lemma: any_field_is_integ_dom
`∀[r:CRng]. IsIntegDom(r) supposing IsField(r)`

Definition: integ_dom
`IntegDom{i} ==  {r:CRng| IsIntegDom(r)} `

Lemma: integ_dom_wf
`IntegDom{i} ∈ 𝕌'`

Definition: field
`Field{i} ==  {r:CRng| IsField(r)} `

Lemma: field_wf
`Field{i} ∈ 𝕌'`

Definition: rprime
`r-Prime(u) ==  (¬u | 1 in r) ∧ (∀v,w:|r|.  (u | v * w in r `` (u | v in r ∨ u | w in r)))`

Lemma: rprime_wf
`∀[r:RngSig]. ∀[u:|r|].  (r-Prime(u) ∈ ℙ)`

Definition: ideal_p
`S Ideal of R ==  S SubGrp of R↓+gp ∧ (∀a,b:|R|.  ((S a) `` (S (a * b))))`

Lemma: ideal_p_wf
`∀[r:CRng]. ∀[a:|r| ⟶ ℙ].  (a Ideal of r ∈ ℙ)`

Lemma: sq_stable__ideal_p
`∀r:CRng. ∀a:|r| ⟶ ℙ.  ((∀x:|r|. SqStable(a x)) `` SqStable(a Ideal of r))`

Definition: ideal
`Ideal(r){i} ==  {p:|r| ⟶ ℙ| p Ideal of r} `

Lemma: ideal_wf
`∀[r:CRng]. (Ideal(r){i} ∈ 𝕌')`

Definition: zero_ideal
`(0r) ==  λu.(u = 0 ∈ |r|)`

Lemma: zero_ideal_wf
`∀[r:CRng]. ((0r) ∈ Ideal(r){i})`

Definition: one_ideal
`(1r) ==  λu.True`

Lemma: one_ideal_wf
`∀[r:CRng]. ((1r) ∈ Ideal(r){i})`

Definition: princ_ideal
`(a)r ==  λc.∃b:|r|. (c = (a * b) ∈ |r|)`

Lemma: princ_ideal_wf
`∀[r:Rng]. ∀[a:|r|].  ((a)r ∈ Ideal(r){i})`

Lemma: ideal_defines_eqv
`∀r:CRng. ∀[a:|r| ⟶ ℙ]. (a Ideal of r `` EquivRel(|r|;u,v.a (u +r (-r v))))`

Lemma: det_ideal_ap_elim
`∀r:CRng. ∀a:Ideal(r){i}. ∀d:detach_fun(|r|;a).  ((∀w:|r|. SqStable(a w)) `` (∀v:|r|. (↑(d v) `⇐⇒` a v)))`

Lemma: det_ideal_defines_eqv
`∀[r:CRng]. ∀[a:Ideal(r){i}]. ∀[d:detach_fun(|r|;a)].  ((∀w:|r|. SqStable(a w)) `` EquivRel(|r|;u,v.↑(d (u +r (-r v)))))`

Definition: nsgrp_of_ideal
`a↓+nsgp ==  a`

Lemma: nsgrp_of_ideal_wf
`∀[r:CRng]. ∀[a:Ideal(r){i}].  (a↓+nsgp ∈ NormSubGrp{i}(r↓+gp))`

Lemma: ideal-detach-equiv
`∀r:CRng. ∀a:Ideal(r){i}.  ((∀x:|r|. SqStable(a x)) `` (∀d:detach_fun(|r|;a). EquivRel(|r|;x,y.↑(d (x +r (-r y))))))`

Definition: quot_ring_car
`Carrier(r/d) ==  x,y:|r|//(↑(d (x +r (-r y))))`

Lemma: quot_ring_car_wf
`∀[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x)) `` (∀[d:detach_fun(|r|;a)]. (Carrier(r/d) ∈ Type)))`

Lemma: quot_ring_car_qinc
`∀[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x)) `` (∀[d:detach_fun(|r|;a)]. (|r| ⊆r Carrier(r/d))))`

Lemma: quot_ring_car_subtype
`∀[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x)) `` (∀[d:detach_fun(|r|;a)]. (|r| ⊆r Carrier(r/d))))`

Definition: quot_ring
`r / d ==  <Carrier(r/d), λx,y. (d (x +r (-r y))), λx,y. tt, λx,y. (x +r y), 0, λx.(-r x), λx,y. (x * y), 1, λx,y. (inr ⋅\000C )>`

Lemma: quot_ring_sig
`∀[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x)) `` (∀[d:detach_fun(|r|;a)]. (r / d ∈ RngSig)))`

Lemma: quot_ring_wf
`∀[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x)) `` (∀[d:detach_fun(|r|;a)]. (r / d ∈ CRng)))`

Lemma: type_inj_wf_for_qrng
`∀[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x)) `` (∀[d:detach_fun(|r|;a)]. ∀[v:|r|].  ([v]{|r / d|} ∈ |r / d|)))`

Lemma: quot_ring_car_elim
`∀[r:CRng]. ∀[a:Ideal(r){i}].`
`  ((∀x:|r|. SqStable(a x)) `` (∀[d:detach_fun(|r|;a)]. ∀[u,v:|r|].  uiff(u = v ∈ Carrier(r/d);↑(d (u +r (-r v))))))`

Lemma: quot_ring_car_elim_a
`∀r:CRng. ∀a:Ideal(r){i}. ∀d:detach_fun(|r|;a).`
`  ((∀w:|r|. SqStable(a w)) `` (∀u,v:|r|.  (u = v ∈ |r / d| `⇐⇒` a (u +r (-r v)))))`

Lemma: quot_ring_car_elim_b
`∀r:CRng. ∀a:Ideal(r){i}. ∀d:detach_fun(|r|;a).`
`  ((∀w:|r|. SqStable(a w)) `` (∀u,v:|r|.  ([u]{|r / d|} = [v]{|r / d|} ∈ |r / d| `⇐⇒` a (u +r (-r v)))))`

Lemma: all_rng_quot_elim
`∀r:CRng. ∀p:Ideal(r){i}.`
`  ((∀x:|r|. SqStable(p x))`
`  `` (∀d:detach_fun(|r|;p). ∀[F:|r / d| ⟶ ℙ]. ((∀w:|r / d|. SqStable(F[w])) `` (∀w:|r / d|. F[w] `⇐⇒` ∀w:|r|. F[w]))))`

Lemma: all_rng_quot_elim_a
`∀r:CRng. ∀p:Ideal(r){i}.`
`  ((∀x:|r|. SqStable(p x))`
`  `` (∀d:detach_fun(|r|;p)`
`        ∀[F:|r / d| ⟶ ℙ]. ((∀w:|r / d|. SqStable(F[w])) `` (∀w:|r / d|. F[w] `⇐⇒` ∀w:|r|. F[[w]{|r / d|}]))))`

Lemma: rng_car_qinc
`∀[r:CRng]. ∀[a:Ideal(r){i}].  ((∀x:|r|. SqStable(a x)) `` (∀[d:detach_fun(|r|;a)]. (|r| ⊆r |r / d|)))`

Definition: prime_ideal_p
`IsPrimeIdeal(R;P) ==  (¬(P 1)) ∧ (∀a,b:|R|.  ((P (a * b)) `` ((P a) ∨ (P b))))`

Lemma: prime_ideal_p_wf
`∀[r:RngSig]. ∀[P:|r| ⟶ ℙ].  (IsPrimeIdeal(r;P) ∈ ℙ)`

Lemma: sq_stable__prime_ideal
`∀r:CRng. ∀p:Ideal(r){i}.  ((∀u:|r|. Dec(p u)) `` SqStable(IsPrimeIdeal(r;p)))`

Definition: max_ideal_p
`IsMaxIdeal(r;m) ==  ∀u:|r|. (¬(m u) `⇐⇒` ∃v:|r|. (m ((u * v) +r (-r 1))))`

Lemma: max_ideal_p_wf
`∀[r:RngSig]. ∀[m:|r| ⟶ ℙ].  (IsMaxIdeal(r;m) ∈ ℙ)`

Definition: rng_hom_p
`(compound):: rng_hom_p(r;s;f) ==  FunThru2op(|r|;|s|;+r;+s;f) ∧ FunThru2op(|r|;|s|;*;*;f) ∧ ((f 1) = 1 ∈ |s|)`

Lemma: rng_hom_p_wf
`∀[r,s:RngSig]. ∀[f:|r| ⟶ |s|].  (rng_hom_p(r;s;f) ∈ ℙ)`

Lemma: rng_hom_zero
`∀[r,s:Rng]. ∀[f:|r| ⟶ |s|].  f[0] = 0 ∈ |s| supposing rng_hom_p(r;s;f)`

Lemma: rng_hom_minus
`∀[r,s:Rng]. ∀[f:|r| ⟶ |s|].  ∀[x:|r|]. (f[-r x] = (-s f[x]) ∈ |s|) supposing rng_hom_p(r;s;f)`

Definition: rng_chom_p
`(compound):: rng_chom_p(r;s;f) ==  rng_hom_p(r;s;f) ∧ (∀a,b:|r|.  (((f a) * (f b)) = ((f b) * (f a)) ∈ |s|))`

Lemma: rng_chom_p_wf
`∀[r,s:RngSig]. ∀[f:|r| ⟶ |s|].  (rng_chom_p(r;s;f) ∈ ℙ)`

Definition: ring_hom
`RingHom(R;S) ==  {f:|R| ⟶ |S|| FunThru2op(|R|;|S|;+R;+S;f) ∧ FunThru2op(|R|;|S|;*;*;f) ∧ ((f 1) = 1 ∈ |S|)} `

Lemma: ring_hom_wf
`∀[r,s:RngSig].  (RingHom(r;s) ∈ ℙ)`

Definition: ring_quot_hom
`nat(r;a) ==  λx.x`

Lemma: idom_alt_char
`∀r:CRng`
`  ((∀x,y:|r|.  Dec(x = y ∈ |r|))`
`  `` (IsIntegDom(r) `⇐⇒` 0 ≠ 1 ∈ |r|  ∧ (∀u,v:|r|.  (u = 0 ∈ |r|) ∨ (v = 0 ∈ |r|) supposing (u * v) = 0 ∈ |r|)))`

Lemma: quot_by_prime_ideal
`∀r:CRng. ∀p:Ideal(r){i}. ∀d:detach_fun(|r|;p).  ((∀u:|r|. SqStable(p u)) `` (IsPrimeIdeal(r;p) `⇐⇒` IsIntegDom(r / d)))`

Lemma: princ_ideal_mem_cond
`∀r:CRng. ∀u,v:|r|.  (v | u in r `⇐⇒` (v)r u)`

Lemma: ideal_of_prime
`∀r:CRng. ∀u:|r|.  (r-Prime(u) `⇐⇒` IsPrimeIdeal(r;(u)r))`

Definition: int_ring
`ℤ-rng ==`
`  <ℤ, λ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 \000C(u ÷ v) fi >`

Lemma: int_ring_wf
`ℤ-rng ∈ IntegDom{i}`

Definition: int_pi_det_fun
`(i)ℤ-det-fun ==  λj.(if (i =z 0) then j else j rem i fi  =z 0)`

Lemma: int_pi_det_fun_wf
`∀[i:ℤ]. ((i)ℤ-det-fun ∈ detach_fun(|ℤ-rng|;(i)ℤ-rng))`

Lemma: int_pi_detach
`∀i:ℤ. ℤ-Detach((i)ℤ-rng)`

Lemma: prime_ideals_in_int_ring
`∀i:ℕ+. (ℤ-rng-Prime(i) `⇐⇒` prime(i))`

Definition: choose
`choose(n;i) ==  Y (λchoose,n,i. if (i =z 0) ∨b(i =z n) then 1 else (choose (n - 1) (i - 1)) + (choose (n - 1) i) fi ) n \000Ci`

Lemma: choose_wf
`∀[n:ℕ]. ∀[i:{0...n}].  (choose(n;i) ∈ ℕ)`

Lemma: comb_for_choose_wf
`λn,i,z. choose(n;i) ∈ n:ℕ ⟶ i:{0...n} ⟶ (↓True) ⟶ ℕ`

Definition: rng_nexp
`e ↑r n ==  n ⋅ e`

Lemma: rng_nexp_wf
`∀[r:Rng]. ∀[n:ℕ]. ∀[u:|r|].  (u ↑r n ∈ |r|)`

Lemma: comb_for_rng_nexp_wf
`λr,n,u,z. (u ↑r n) ∈ r:Rng ⟶ n:ℕ ⟶ u:|r| ⟶ (↓True) ⟶ |r|`

Definition: rng_nat_op
`n ⋅r e ==  n ⋅ e`

Lemma: rng_nat_op_wf
`∀[r:Rng]. ∀[n:ℕ]. ∀[u:|r|].  (n ⋅r u ∈ |r|)`

Lemma: comb_for_rng_nat_op_wf
`λr,n,u,z. (n ⋅r u) ∈ r:Rng ⟶ n:ℕ ⟶ u:|r| ⟶ (↓True) ⟶ |r|`

Lemma: rng_nat_op-int
`∀[n:ℕ]. ∀[a:ℤ].  (n ⋅ℤ-rng a ~ n * a)`

Lemma: rng_nexp-int
`∀[n:ℕ]. ∀[a:ℤ].  ((a ↑ℤ-rng n) = a^n ∈ ℤ)`

Definition: int-to-ring
`int-to-ring(r;n) ==  if n <z 0 then -r ((-n) ⋅r 1) else n ⋅r 1 fi `

Lemma: int-to-ring_wf
`∀[r:Rng]. ∀[n:ℤ].  (int-to-ring(r;n) ∈ |r|)`

Lemma: int-to-ring-zero
`∀[r:Top]. (int-to-ring(r;0) ~ 0)`

Lemma: int-to-ring-one
`∀[r:Rng]. (int-to-ring(r;1) = 1 ∈ |r|)`

Lemma: int-to-ring-minus-one
`∀[r:Rng]. (int-to-ring(r;-1) = (-r 1) ∈ |r|)`

Lemma: int-to-ring-int
`∀[x:ℤ]. (int-to-ring(ℤ-rng;x) = x ∈ ℤ)`

Lemma: rng_nexp_zero
`∀[r:Rng]. ∀[e:|r|].  ((e ↑r 0) = 1 ∈ |r|)`

Lemma: rng_nexp_unroll
`∀[r:Rng]. ∀[n:ℕ+]. ∀[e:|r|].  ((e ↑r n) = ((e ↑r (n - 1)) * e) ∈ |r|)`

Lemma: rng_nat_op_one
`∀[r:Rng]. ∀[e:|r|].  ((1 ⋅r e) = e ∈ |r|)`

`∀[r:Rng]. ∀[e:|r|]. ∀[a,b:ℕ].  (((a + b) ⋅r e) = ((a ⋅r e) +r (b ⋅r e)) ∈ |r|)`

`∀[r:Rng]. ∀[a1,a2:ℤ].  (int-to-ring(r;a1 + a2) = (int-to-ring(r;a1) +r int-to-ring(r;a2)) ∈ |r|)`

Lemma: int-to-ring-minus
`∀[r:Rng]. ∀[y:ℤ].  (int-to-ring(r;-y) = (-r int-to-ring(r;y)) ∈ |r|)`

Lemma: int-to-ring-mul
`∀[r:Rng]. ∀[a1,a2:ℤ].  (int-to-ring(r;a1 * a2) = (int-to-ring(r;a1) * int-to-ring(r;a2)) ∈ |r|)`

Lemma: int-to-ring-hom
`∀[r:Rng]. rng_hom_p(ℤ-rng;r;λx.int-to-ring(r;x))`

Lemma: rng_sum_unroll_empty
`∀[r:Rng]. ∀[i,j:ℤ].  ∀[E:{i..j-} ⟶ |r|]. ((Σ(r) i ≤ k < j. E[k]) = 0 ∈ |r|) supposing j ≤ i`

Lemma: rng_sum_unroll_base
`∀[r:Rng]. ∀[i,j:ℤ].  ∀[E:{i..j-} ⟶ |r|]. ((Σ(r) i ≤ k < j. E[k]) = 0 ∈ |r|) supposing i = j ∈ ℤ`

Lemma: rng_sum_unroll_hi
`∀[r:Rng]. ∀[i,j:ℤ].`
`  ∀[E:{i..j-} ⟶ |r|]. ((Σ(r) i ≤ k < j. E[k]) = ((Σ(r) i ≤ k < j - 1. E[k]) +r E[j - 1]) ∈ |r|) supposing i < j`

Lemma: rng_sum_unroll_unit
`∀[r:Rng]. ∀[i,j:ℤ].  ∀[E:{i..j-} ⟶ |r|]. ((Σ(r) i ≤ k < j. E[k]) = E[i] ∈ |r|) supposing (i + 1) = j ∈ ℤ`

Lemma: rng_sum_unroll_lo
`∀[r:Rng]. ∀[i,j:ℤ].`
`  ∀[E:{i..j-} ⟶ |r|]. ((Σ(r) i ≤ k < j. E[k]) = (E[i] +r (Σ(r) i + 1 ≤ k < j. E[k])) ∈ |r|) supposing i < j`

Lemma: rng_sum_single
`∀[r:Rng]. ∀[i,j:ℤ].  ∀[E:{i..j-} ⟶ |r|]. ((Σ(r) i ≤ k < j. E[k]) = E[i] ∈ |r|) supposing j = (i + 1) ∈ ℤ`

Lemma: rng_sum_shift
`∀[r:Rng]. ∀[a,b:ℤ].`
`  ∀[E:{a..b-} ⟶ |r|]. ∀[k:ℤ].  ((Σ(r) a ≤ j < b. E[j]) = (Σ(r) a + k ≤ j < b + k. E[j - k]) ∈ |r|) supposing a ≤ b`

Lemma: rng_sum_split
`∀[r:Rng]. ∀[a,b,c:ℤ].`
`  (∀[E:{a..c-} ⟶ |r|]. ((Σ(r) a ≤ j < c. E[j]) = ((Σ(r) a ≤ j < b. E[j]) +r (Σ(r) b ≤ j < c. E[j])) ∈ |r|)) supposing `
`     ((b ≤ c) and `
`     (a ≤ b))`

Lemma: rng_sum_plus
`∀[r:Rng]. ∀[a,b:ℤ].`
`  ∀[E,F:{a..b-} ⟶ |r|].  ((Σ(r) a ≤ i < b. E[i] +r F[i]) = ((Σ(r) a ≤ i < b. E[i]) +r (Σ(r) a ≤ i < b. F[i])) ∈ |r|) `
`  supposing a ≤ b`

Lemma: rng_sum_swap
`∀[r:Rng]. ∀[k,m:ℕ]. ∀[F:ℕm ⟶ ℕk ⟶ |r|].`
`  ((Σ(r) 0 ≤ i < m. Σ(r) 0 ≤ j < k. F[i;j]) = (Σ(r) 0 ≤ j < k. Σ(r) 0 ≤ i < m. F[i;j]) ∈ |r|)`

Lemma: rng_times_sum_l
`∀[r:Rng]. ∀[a,b:ℤ].`
`  ∀[E:{a..b-} ⟶ |r|]. ∀[u:|r|].  ((u * (Σ(r) a ≤ j < b. E[j])) = (Σ(r) a ≤ j < b. u * E[j]) ∈ |r|) supposing a ≤ b`

Lemma: rng_times_sum_r
`∀[r:Rng]. ∀[a,b:ℤ].`
`  ∀[E:{a..b-} ⟶ |r|]. ∀[u:|r|].  (((Σ(r) a ≤ j < b. E[j]) * u) = (Σ(r) a ≤ j < b. E[j] * u) ∈ |r|) supposing a ≤ b`

Lemma: rng_minus_sum
`∀[r:Rng]. ∀[a,b:ℤ].`
`  ∀[F:{a..b-} ⟶ |r|]. ((-r (Σ(r) a ≤ i < b. F[i])) = (Σ(r) a ≤ i < b. -r F[i]) ∈ |r|) supposing a ≤ b`

Lemma: rng_sum_0
`∀[r:Rng]. ∀[a,b:ℤ].  (Σ(r) a ≤ j < b. 0) = 0 ∈ |r| supposing a ≤ b`

Lemma: rng_sum_is_0
`∀[r:Rng]. ∀[a,b:ℤ]. ∀[F:{a..b-} ⟶ |r|].`
`  (Σ(r) a ≤ j < b. F[j]) = 0 ∈ |r| supposing (a ≤ b) ∧ (∀j:{a..b-}. (F[j] = 0 ∈ |r|))`

Lemma: rng_times_nat_op
`∀[r:Rng]. ∀[a,b:|r|]. ∀[n:ℕ].  ((a * (n ⋅r b)) = (n ⋅r (a * b)) ∈ |r|)`

Lemma: rng_times_nat_op_r
`∀[r:Rng]. ∀[a,b:|r|]. ∀[n:ℕ].  (((n ⋅r b) * a) = (n ⋅r (b * a)) ∈ |r|)`

Lemma: binomial
`∀[r:CRng]. ∀[a,b:|r|]. ∀[n:ℕ].`
`  (((a +r b) ↑r n) = (Σ(r) 0 ≤ i < n + 1. choose(n;i) ⋅r ((a ↑r i) * (b ↑r (n - i)))) ∈ |r|)`

Lemma: sum_of_geometric_prog
`∀[r:CRng]. ∀[a:|r|]. ∀[n:ℕ].  (((1 +r (-r a)) * (Σ(r) 0 ≤ i < n. a ↑r i)) = (1 +r (-r (a ↑r n))) ∈ |r|)`

Definition: rng_when
`when b. p ==  when b. p`

Lemma: rng_when_wf
`∀[r:Rng]. ∀[b:𝔹]. ∀[p:|r|].  (when b. p ∈ |r|)`

Lemma: comb_for_rng_when_wf
`λr,b,p,z. (when b. p) ∈ r:Rng ⟶ b:𝔹 ⟶ p:|r| ⟶ (↓True) ⟶ |r|`

Lemma: rng_times_when_l
`∀[r:Rng]. ∀[u,v:|r|]. ∀[b:𝔹].  ((u * (when b. v)) = (when b. (u * v)) ∈ |r|)`

Lemma: rng_times_when_r
`∀[r:Rng]. ∀[u,v:|r|]. ∀[b:𝔹].  (((when b. u) * v) = (when b. (u * v)) ∈ |r|)`

Lemma: rng_when_of_zero
`∀[r:Rng]. ∀[b:𝔹].  ((when b. 0) = 0 ∈ |r|)`

Lemma: rng_when_thru_plus
`∀[r:Rng]. ∀[b:𝔹]. ∀[p,q:|r|].  ((when b. (p +r q)) = ((when b. p) +r (when b. q)) ∈ |r|)`

Lemma: rng_when_when
`∀[r:Rng]. ∀[b,b':𝔹]. ∀[p:|r|].  ((when b. when b'. p) = (when b ∧b b'. p) ∈ |r|)`

Lemma: rng_when_swap
`∀[r:Rng]. ∀[b,b':𝔹]. ∀[p:|r|].  ((when b. when b'. p) = (when b'. when b. p) ∈ |r|)`

Definition: ring_term_value
`ring_term_value(f;t) ==`
`  int_term_ind(t;`
`               itermConstant(n)`` int-to-ring(r;n);`
`               itermVar(v)`` f v;`
`               itermAdd(a,b)`` av,bv.av +r bv;`
`               itermSubtract(a,b)`` av,bv.av +r (-r bv);`
`               itermMultiply(a,b)`` av,bv.av * bv;`
`               itermMinus(a)`` av.-r av) `

Lemma: ring_term_value_wf
`∀[r:Rng]. ∀[f:ℤ ⟶ |r|]. ∀[t:int_term()].  (ring_term_value(f;t) ∈ |r|)`

`∀r,b,a,f:Top.  (ring_term_value(f;a (+) b) ~ ring_term_value(f;a) +r ring_term_value(f;b))`

Lemma: ring_term_value_mul_lemma
`∀r,b,a,f:Top.  (ring_term_value(f;a (*) b) ~ ring_term_value(f;a) * ring_term_value(f;b))`

Lemma: ring_term_value_minus_lemma
`∀r,a,f:Top.  (ring_term_value(f;"-"a) ~ -r ring_term_value(f;a))`

Lemma: ring_term_value_const_lemma
`∀r,a,f:Top.  (ring_term_value(f;"a") ~ int-to-ring(r;a))`

Lemma: ring_term_value_var_lemma
`∀r,c,f:Top.  (ring_term_value(f;vc) ~ f c)`

Lemma: ring_term_value_sub_lemma
`∀r,b,a,f:Top.  (ring_term_value(f;a (-) b) ~ ring_term_value(f;a) +r (-r ring_term_value(f;b)))`

Definition: ringeq_int_terms
`t1 ≡ t2 ==  ∀f:ℤ ⟶ |r|. (ring_term_value(f;t1) = ring_term_value(f;t2) ∈ |r|)`

Lemma: ringeq_int_terms_wf
`∀[t1,t2:int_term()]. ∀[r:Rng].  (t1 ≡ t2 ∈ ℙ)`

Lemma: ringeq_int_terms_functionality
`∀[r:Rng]. ∀[x1,x2,y1,y2:int_term()].  (uiff(x1 ≡ y1;x2 ≡ y2)) supposing (y1 ≡ y2 and x1 ≡ x2)`

Lemma: ringeq_int_terms_weakening
`∀[r:Rng]. ∀[t1,t2:int_term()].  t1 ≡ t2 supposing t1 = t2 ∈ int_term()`

Lemma: ringeq_int_terms_transitivity
`∀[r:Rng]. ∀[t1,t2,t3:int_term()].  (t1 ≡ t3) supposing (t2 ≡ t3 and t1 ≡ t2)`

Lemma: ringeq_int_terms_inversion
`∀[r:Rng]. ∀[t1,t2:int_term()].  t1 ≡ t2 supposing t2 ≡ t1`

`∀[r:Rng]. ∀[a,b,c,d:int_term()].  (a (+) c ≡ b (+) d) supposing (a ≡ b and c ≡ d)`

Lemma: itermSubtract_functionality_wrt_ringeq
`∀[r:Rng]. ∀[a,b,c,d:int_term()].  (a (-) c ≡ b (-) d) supposing (a ≡ b and c ≡ d)`

Lemma: itermMinus_functionality_wrt_ringeq
`∀[r:Rng]. ∀[a,b:int_term()].  "-"a ≡ "-"b supposing a ≡ b`

Lemma: itermMultiply_functionality_wrt_ringeq
`∀[r:Rng]. ∀[a,b,c,d:int_term()].  (a (*) c ≡ b (*) d) supposing (a ≡ b and c ≡ d)`

Lemma: imonomial-ringeq-lemma
`∀r:Rng. ∀f:ℤ ⟶ |r|. ∀ws:ℤ List. ∀t:int_term().`
`  (ring_term_value(f;accumulate (with value t and list item v):`
`                      t (*) vv`
`                     over list:`
`                       ws`
`                     with starting value:`
`                      t))`
`  = (ring_term_value(f;t) `
`     * `
`     ring_term_value(f;accumulate (with value t and list item v):`
`                        t (*) vv`
`                       over list:`
`                         ws`
`                       with starting value:`
`                        "1")))`
`  ∈ |r|)`

Lemma: imonomial-term-linear-ringeq
`∀r:Rng. ∀f:ℤ ⟶ |r|. ∀ws:ℤ List. ∀c:ℤ.  (ring_term_value(f;imonomial-term(<c, ws>)) = (int-to-ring(r;c) * ring_term_valu\000Ce(f;imonomial-term(<1, ws>))) ∈ |r|)`

`∀r:Rng. ∀vs:ℤ List. ∀a,b:ℤ-o. ∀f:ℤ ⟶ |r|.  ((ring_term_value(f;imonomial-term(<a, vs>)) +r ring_term_value(f;imonomial-\000Cterm(<b, vs>))) = ring_term_value(f;imonomial-term(<a + b, vs>)) ∈ |r|)`

Lemma: ipolynomial-term-cons-ringeq
`∀[r:Rng]. ∀[m:iMonomial()]. ∀[p:iMonomial() List].`
`  ipolynomial-term([m / p]) ≡ imonomial-term(m) (+) ipolynomial-term(p)`

`∀r:Rng. ∀p,q:iMonomial() List.  ipolynomial-term(add-ipoly(p;q)) ≡ ipolynomial-term(p) (+) ipolynomial-term(q)`

Lemma: minus-poly-ringeq
`∀r:Rng. ∀p:iPolynomial().  ipolynomial-term(minus-poly(p)) ≡ "-"ipolynomial-term(p)`

Lemma: imonomial-cons-ringeq
`∀r:CRng. ∀v:ℤ List. ∀u,a:ℤ. ∀f:ℤ ⟶ |r|.  (ring_term_value(f;imonomial-term(<a, [u / v]>)) = ((f u) * ring_term_value(f;\000Cimonomial-term(<a, v>))) ∈ |r|)`

Lemma: mul-monomials-ringeq
`∀[r:CRng]. ∀[m1,m2:iMonomial()].  imonomial-term(mul-monomials(m1;m2)) ≡ imonomial-term(m1) (*) imonomial-term(m2)`

Lemma: mul-mono-poly-ringeq
`∀[r:CRng]. ∀[m:iMonomial()]. ∀[p:iMonomial() List].`
`  ipolynomial-term(mul-mono-poly(m;p)) ≡ imonomial-term(m) (*) ipolynomial-term(p)`

Lemma: mul-ipoly-ringeq
`∀r:CRng. ∀p,q:iMonomial() List.  ipolynomial-term(mul-ipoly(p;q)) ≡ ipolynomial-term(p) (*) ipolynomial-term(q)`

Lemma: ring_term_polynomial
`∀r:CRng. ∀t:int_term().  ipolynomial-term(int_term_to_ipoly(t)) ≡ t`

Lemma: ring_polynomial_null
`∀r:CRng. ∀t:int_term().  t ≡ "0" supposing inl Ax ≤ null(int_term_to_ipoly(t))`

Lemma: ringeq-iff-rsub-is-0
`∀[r:Rng]. ∀[a,b:|r|].  uiff(a = b ∈ |r|;(a +r (-r b)) = 0 ∈ |r|)`

Lemma: test-ring-eq
`∀[r:CRng]`
`  ∀v,v1,v2,v3,v4,v5,v6,v7,v8,v9:|r|.`
`    ((((((v6 * v3) +r ((v2 * v5) +r (v4 * v7))) +r (-r ((v7 * v2) +r ((v3 * v4) +r (v5 * v6))))) `
`       * `
`       (((v6 * v9) +r ((v8 * v1) +r (v * v7))) +r (-r ((v7 * v8) +r ((v9 * v) +r (v1 * v6)))))) `
`      +r `
`      (((((v * v7) +r ((v6 * v5) +r (v4 * v1))) +r (-r ((v1 * v6) +r ((v7 * v4) +r (v5 * v))))) `
`        * `
`        (((v6 * v9) +r ((v8 * v3) +r (v2 * v7))) +r (-r ((v7 * v8) +r ((v9 * v2) +r (v3 * v6)))))) `
`       +r `
`       ((((v * v3) +r ((v2 * v7) +r (v6 * v1))) +r (-r ((v1 * v2) +r ((v3 * v6) +r (v7 * v))))) `
`        * `
`        (((v6 * v9) +r ((v8 * v5) +r (v4 * v7))) +r (-r ((v7 * v8) +r ((v9 * v4) +r (v5 * v6))))))))`
`    = 0`
`    ∈ |r|)`

`p-adics(p) ==  {f:n:ℕ+ ⟶ ℕp^n| ∀n:ℕ+. ((f (n + 1)) ≡ (f n) mod p^n)} `

`∀[p:ℤ]. (p-adics(p) ∈ Type)`

Definition: p-reduce
`i mod(p^n) ==  i mod p^n`

Lemma: p-reduce_wf
`∀[p:ℕ+]. ∀[n:ℕ]. ∀[i:ℤ].  (i mod(p^n) ∈ ℕp^n)`

Lemma: p-reduce-eqmod
`∀p:ℕ+. ∀n:ℕ. ∀i:ℤ.  (i mod(p^n) ≡ i mod p^n)`

Lemma: p-reduce-self
`∀p:ℕ+. ∀n:ℕ.  (p^n mod(p^n) = 0 ∈ ℤ)`

Lemma: p-reduce-0
`∀p:ℕ+. ∀n:ℕ.  (0 mod(p^n) = 0 ∈ ℤ)`

Lemma: p-reduce-eqmod-exp
`∀p:ℕ+. ∀n:ℕ. ∀m:{n...}. ∀z:ℤ.  (z mod(p^m) ≡ z mod p^n)`

`x + y ==  λn.(x n) + (y n) mod(p^n)`

`∀[p:ℕ+]. ∀[x,y:p-adics(p)].  (x + y ∈ p-adics(p))`

Definition: p-mul
`x * y ==  λn.(x n) * (y n) mod(p^n)`

Lemma: p-mul_wf
`∀[p:ℕ+]. ∀[x,y:p-adics(p)].  (x * y ∈ p-adics(p))`

Definition: p-minus
`-(x) ==  λn.-(x n) mod(p^n)`

Lemma: p-minus_wf
`∀[p:ℕ+]. ∀[x:p-adics(p)].  (-(x) ∈ p-adics(p))`

`∀[p:ℕ+]. (p-adics(p) ⊆r (ℕ+ ⟶ ℤ))`

`∀[p:ℕ+]. ∀[x,y:p-adics(p)].  uiff(x = y ∈ p-adics(p);x = y ∈ (ℕ+ ⟶ ℤ))`

`∀p:ℕ+. ∀x,y:p-adics(p).  uiff(x = y ∈ p-adics(p);∀n:ℕ+. ((x n) ≡ (y n) mod p^n))`

Definition: p-int
`k(p) ==  λn.k mod(p^n)`

Lemma: p-int_wf
`∀[p:ℕ+]. ∀[k:ℤ].  (k(p) ∈ p-adics(p))`

`∀[p:ℕ+]. ∀[k,j:ℤ].  (k(p) + j(p) = k + j(p) ∈ p-adics(p))`

Lemma: p-mul-int
`∀[p:ℕ+]. ∀[k,j:ℤ].  (k(p) * j(p) = k * j(p) ∈ p-adics(p))`

Lemma: p-minus-int
`∀[p:ℕ+]. ∀[k:ℤ].  (-(k(p)) = -k(p) ∈ p-adics(p))`

Lemma: p-int-eventually-constant
`∀p:{2...}. ∀k:ℕ.  ∃n:ℕ+. ∀m:{n...}. ((k(p) m) = k ∈ ℤ)`

Lemma: p-minus-int-eventually
`∀p:{2...}. ∀k:ℕ+.  ∃n:ℕ+. ∀m:{n...}. ((-k(p) m) = (p^m - k) ∈ ℤ)`

Lemma: p-int-injection
`∀[p:{2...}]. Inj(ℤ;p-adics(p);λk.k(p))`

`∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+. ∀m:{n...}.  ((a m) ≡ (a n) mod p^n)`

`∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+.  ((0 ≤ ((a (n + 1)) - a n)) ∧ (((a (n + 1)) - a n) ≤ (p^(n + 1) - p^n)))`

`∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+. ∀i:ℕ+n + 1.  ((a i) ≤ (a n))`

`∀p:{p:{2...}| prime(p)} . ∀a:{a:p-adics(p)| ¬((a 1) = 0 ∈ ℤ)} . ∀n:ℕ+.  (∃c:ℕp^n [((c * (a n)) ≡ 1 mod p^n)])`

`∀p:{p:{2...}| prime(p)} . ∀a:{a:p-adics(p)| ¬((a 1) = 0 ∈ ℤ)} . ∀n:ℕ+.  (∃c:ℕp^n [((c * (a n)) ≡ 1 mod p^n)])`

Definition: p-units
`p-units(p) ==  {a:p-adics(p)| ¬((a 1) = 0 ∈ ℤ)} `

Lemma: p-units_wf
`∀[p:ℤ]. (p-units(p) ∈ Type)`

Definition: p-inv
`p-inv(p;a) ==`
`  λn.eval pn = p^n in`
`     eval an = a n in`
`       let x,y = letrec rec(p)=λq.if p=0`
`                                  then <q, 0, 1, 1, 1, Ax, Ax, Ax>`
`                                  else let x,y = divrem(q; p) `
`                                       in eval r = y in`
`                                          let g,t = rec r p `
`                                          in let a,b,x1,y1,_,_,_@0 = t in `
`                                              eval q' = x in`
`                                              eval b' = (b * q') + a in`
`                                              eval x' = y1 - x1 * q' in`
`                                                <g, b, b', x', x1, Ax, Ax, Ax> in`
`                  rec(|a n|) `
`                 pn `
`       in let x1,x2,x3,x4,x5,x5,y = y in `
`           eval r = 1 * x3 rem pn in`
`           if (r) < (0)  then pn + r  else r`

Lemma: p-inv_wf
`∀p:{p:{2...}| prime(p)} . ∀a:p-units(p).  (p-inv(p;a) ∈ {b:p-adics(p)| a * b = 1(p) ∈ p-adics(p)} )`

`ℤ(p) ==  <p-adics(p), λu,v. ff, λu,v. ff, λu,v. u + v, 0(p), λu.-(u), λu,v. u * v, 1(p), λu,v. (inr ⋅ )>`

`∀[p:{2...}]. (ℤ(p) ∈ CRng)`

Lemma: p-mul-assoc
`∀[p:{2...}]. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))`

`∀[p:{2...}]. ∀[x,y,z:p-adics(p)].  (x + y + z = x + y + z ∈ p-adics(p))`

Lemma: p-distrib
`∀[p:{2...}]. ∀[a,x,y:p-adics(p)].  ((a * x + y = a * x + a * y ∈ p-adics(p)) ∧ (x + y * a = x * a + y * a ∈ p-adics(p)))`

Lemma: p-mul-comm
`∀[p:{2...}]. ∀[x,y:p-adics(p)].  (x * y = y * x ∈ p-adics(p))`

Lemma: p-mul-1
`∀[p:{2...}]. ∀[a:p-adics(p)].  (1(p) * a = a ∈ p-adics(p))`

Lemma: p-1-mul
`∀[p:{2...}]. ∀[a:p-adics(p)].  (a * 1(p) = a ∈ p-adics(p))`

`∀[p:{2...}]. (λk.k(p) ∈ RingHom(ℤ-rng;ℤ(p)))`

Definition: p-digit
`p-digit(p;a;n) ==  if (n =z 1) then a 1 else ((a n) - a (n - 1)) ÷ p^n - 1 fi `

Lemma: p-digit_wf
`∀[p:ℕ+]. ∀[a:p-adics(p)]. ∀[n:ℕ+].  (p-digit(p;a;n) ∈ ℕp)`

Definition: p-digits
`p-digits(p;a) ==  λn.p-digit(p;a;n)`

Lemma: p-digits_wf
`∀[p:ℕ+]. ∀[a:p-adics(p)].  (p-digits(p;a) ∈ ℕ+ ⟶ ℕp)`

Definition: p-shift
`p-shift(p;a;k) ==  λn.((a (n + k)) ÷ p^k)`

Lemma: p-shift_wf
`∀[p:ℕ+]. ∀[a:p-adics(p)]. ∀[k:ℕ+].  p-shift(p;a;k) ∈ p-adics(p) supposing (a k) = 0 ∈ ℤ`

Lemma: p-shift-mul
`∀[p:ℕ+]. ∀[a:p-adics(p)]. ∀[k:ℕ+].  p^k(p) * p-shift(p;a;k) = a ∈ p-adics(p) supposing (a k) = 0 ∈ ℤ`

Lemma: p-shift-0
`∀p,n:ℕ+.  (p-shift(p;0(p);n) = 0(p) ∈ p-adics(p))`

Definition: greatest-p-zero
`greatest-p-zero(n;a) ==  primrec(n;0;λi,v. if (a (i + 1) =z 0) then i + 1 else v fi )`

Lemma: greatest-p-zero_wf
`∀[a:ℕ+ ⟶ ℤ]. ∀[n:ℕ].  (greatest-p-zero(n;a) ∈ ℕ)`

Lemma: greatest-p-zero-property
`∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ.`
`  ((greatest-p-zero(n;a) ≤ n)`
`  ∧ (∀i:ℕ+n + 1. (((i ≤ greatest-p-zero(n;a)) `` ((a i) = 0 ∈ ℤ)) ∧ (greatest-p-zero(n;a) < i `` (¬((a i) = 0 ∈ ℤ))))))`

Lemma: shift-greatest-p-zero-unit
`∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+.`
`  ((¬((a n) = 0 ∈ ℤ)) `` 0 < greatest-p-zero(n;a) `` (p-shift(p;a;greatest-p-zero(n;a)) ∈ p-units(p)))`

Definition: p-unitize
`p-unitize(p;a;n) ==  eval k = greatest-p-zero(n;a) in <k, if k=0 then a else p-shift(p;a;k)>`

Lemma: p-unitize_wf
`∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+.`
`  ((¬((a n) = 0 ∈ ℤ)) `` (p-unitize(p;a;n) ∈ k:ℕn + 1 × {b:p-units(p)| p^k(p) * b = a ∈ p-adics(p)} ))`

Lemma: p-unitize-unit
`∀p:ℕ+. ∀a:p-units(p). ∀n:ℕ+.  (p-unitize(p;a;n) = <0, a> ∈ (k:ℕ × {b:p-units(p)| p^k(p) * b = a ∈ p-adics(p)} ))`

Lemma: p-mul-int-cancelation-1
`∀[p:{2...}]. ∀[k:ℕ]. ∀[a,b:p-adics(p)].  ((p^k(p) * a = p^k(p) * b ∈ p-adics(p)) `` (a = b ∈ p-adics(p)))`

Lemma: p-mul-int-cancelation-2
`∀[p:{p:{2...}| prime(p)} ]. ∀[k:ℕ]. ∀[a,b:p-adics(p)].`
`  (a = b ∈ p-adics(p)) supposing ((k(p) * a = k(p) * b ∈ p-adics(p)) and CoPrime(k,p))`

Lemma: p-unit-part-unique
`∀[p:{2...}]. ∀[k,j:ℕ]. ∀[a,b:p-units(p)].`
`  (a = b ∈ p-units(p)) ∧ (k = j ∈ ℤ) supposing p^k(p) * a = p^j(p) * b ∈ p-adics(p)`

Definition: p-sep
`p-sep(x;y) ==  ∃n:ℕ+. (¬((x n) = (y n) ∈ ℤ))`

Lemma: p-sep_wf
`∀[p:ℕ+]. ∀[x,y:p-adics(p)].  (p-sep(x;y) ∈ ℙ)`

Lemma: p-sep-or
`∀[p:ℕ+]. ∀[x:p-adics(p)].  ∀y:p-adics(p). (p-sep(x;y) `` (∀z:p-adics(p). (p-sep(z;x) ∨ p-sep(z;y))))`

Lemma: p-sep-irrefl
`∀[p:ℕ+]. ∀[x:p-adics(p)].  (¬p-sep(x;x))`

Lemma: p-unit-iff
`∀p:{p:{2...}| prime(p)} . ∀a:p-adics(p).  (¬((a 1) = 0 ∈ ℤ) `⇐⇒` ∃b:p-adics(p). (a * b = 1(p) ∈ p-adics(p)))`

`basic-padic(p) ==  ℕ × p-adics(p)`

`∀[p:ℤ]. (basic-padic(p) ∈ Type)`

`bpa-add(p;x;y) ==`
`  let n,a = x `
`  in let m,b = y `
`     in eval k = imax(n;m) in`
`        eval c = p^k - n in`
`        eval d = p^k - m in`
`          <k, c(p) * a + d(p) * b>`

`∀[p:ℕ+]. ∀[x,y:basic-padic(p)].  (bpa-add(p;x;y) ∈ basic-padic(p))`

Definition: bpa-mul
`bpa-mul(p;x;y) ==  let n,a = x in let m,b = y in <n + m, a * b>`

Lemma: bpa-mul_wf
`∀[p:ℕ+]. ∀[x,y:basic-padic(p)].  (bpa-mul(p;x;y) ∈ basic-padic(p))`

Definition: bpa-minus
`bpa-minus(p;x) ==  let n,a = x in <n, -(a)>`

Lemma: bpa-minus_wf
`∀[p:ℕ+]. ∀[x:basic-padic(p)].  (bpa-minus(p;x) ∈ basic-padic(p))`

Definition: bpa-equiv
`bpa-equiv(p;x;y) ==  let n,a = x in let m,b = y in p^m(p) * a = p^n(p) * b ∈ p-adics(p)`

Lemma: bpa-equiv_wf
`∀[p:ℕ+]. ∀[x,y:basic-padic(p)].  (bpa-equiv(p;x;y) ∈ ℙ)`

Lemma: bpa-equiv-equiv
`∀[p:{2...}]. EquivRel(basic-padic(p);x,y.bpa-equiv(p;x;y))`

Lemma: bpa-equiv_transitivity
`∀p:{2...}. ∀a,b,c:basic-padic(p).  (bpa-equiv(p;a;b) `` bpa-equiv(p;b;c) `` bpa-equiv(p;a;c))`

Lemma: bpa-equiv_inversion
`∀p:{2...}. ∀a,b:basic-padic(p).  (bpa-equiv(p;a;b) `` bpa-equiv(p;b;a))`

Lemma: bpa-equiv_weakening
`∀p:{2...}. ∀a,b:basic-padic(p).  ((a = b ∈ basic-padic(p)) `` bpa-equiv(p;b;a))`

Definition: bpa-norm
`bpa-norm(p;x) ==`
`  let n,a = x `
`  in if (n =z 0) then <0, a>`
`     if (a n =z 0) then <0, p-shift(p;a;n)>`
`     else let k,b = p-unitize(p;a;n) `
`          in <n - k, b>`
`     fi `

Lemma: bpa-norm_wf
`∀p:ℕ+. ∀x:basic-padic(p).  (bpa-norm(p;x) ∈ basic-padic(p))`

Lemma: bpa-norm-equiv
`∀p:{2...}. ∀x:basic-padic(p).  bpa-equiv(p;x;bpa-norm(p;x))`

Lemma: bpa-equiv-iff-norm
`∀p:{2...}. ∀x,y:basic-padic(p).  (bpa-equiv(p;x;y) `⇐⇒` bpa-norm(p;x) = bpa-norm(p;y) ∈ basic-padic(p))`

`padic(p) ==  n:ℕ × if (n =z 0) then p-adics(p) else p-units(p) fi `

`∀[p:ℤ]. (padic(p) ∈ Type)`

`∀[p:ℤ]. (padic(p) ⊆r basic-padic(p))`

`∀[p:ℕ+]. ∀[x:basic-padic(p)].  (bpa-norm(p;x) ∈ padic(p))`

`∀[p:ℤ]. ∀[x,y:padic(p)].  uiff(x = y ∈ padic(p);x = y ∈ basic-padic(p))`

`∀[p:ℕ+]. ∀[x:padic(p)].  (bpa-norm(p;x) = x ∈ padic(p))`

Lemma: bpa-equiv-iff-norm2
`∀p:{2...}. ∀x,y:basic-padic(p).  (bpa-norm(p;x) = bpa-norm(p;y) ∈ padic(p) `⇐⇒` bpa-equiv(p;x;y))`

`(a/p^n) ==  bpa-norm(p;<n, a>)`

`∀[p:ℕ+]. ∀[n:ℕ]. ∀[a:p-adics(p)].  ((a/p^n) ∈ padic(p))`

`∀[p:{2...}]. ∀[n,m:ℕ]. ∀[a,b:p-adics(p)].  (a/p^n) = (b/p^m) ∈ padic(p) supposing bpa-equiv(p;<n, a>;<m, b>)`

`∀[p:{2...}]. ∀[n:ℕ]. ∀[a:p-adics(p)].  ((a/p^n) ∈ {x:basic-padic(p)| bpa-equiv(p;<n, a>;x)} )`

Definition: pa-int
`k(p) ==  <0, k(p)>`

Lemma: pa-int_wf
`∀[p:{2...}]. ∀[k:ℤ].  (k(p) ∈ padic(p))`

Definition: pa-mul
`pa-mul(p;x;y) ==  bpa-norm(p;bpa-mul(p;x;y))`

Lemma: pa-mul_wf
`∀[p:{2...}]. ∀[x,y:basic-padic(p)].  (pa-mul(p;x;y) ∈ padic(p))`

Lemma: pa-mul_functionality
`∀[p,q:{2...}]. ∀[x1,y1,x2,y2:basic-padic(p)].`
`  (pa-mul(p;x1;y1) = pa-mul(q;x2;y2) ∈ padic(p)) supposing ((p = q ∈ ℤ) and bpa-equiv(p;x1;x2) and bpa-equiv(p;y1;y2))`

`pa-add(p;x;y) ==  bpa-norm(p;bpa-add(p;x;y))`

`∀[p:{2...}]. ∀[x,y:basic-padic(p)].  (pa-add(p;x;y) ∈ padic(p))`

`∀[p:{2...}]. ∀[x1,y1,x2,y2:basic-padic(p)].`
`  (pa-add(p;x1;y1) = pa-add(p;x2;y2) ∈ padic(p)) supposing (bpa-equiv(p;x1;x2) and bpa-equiv(p;y1;y2))`

Definition: pa-minus
`pa-minus(p;x) ==  bpa-norm(p;bpa-minus(p;x))`

Lemma: pa-minus_wf
`∀[p:{2...}]. ∀[x:padic(p)].  (pa-minus(p;x) ∈ padic(p))`

`padic-ring(p) ==  <padic(p), λu,v. ff, λu,v. ff, λu,v. pa-add(p;u;v), 0(p), λu.pa-minus(p;u), λu,v. pa-mul(p;u;v), 1(p),\000C λu,v. (inr ⋅ )>`

`∀[p:{2...}]. (padic-ring(p) ∈ CRng)`

Definition: pa-sep
`pa-sep(p;x;y) ==  let n,a = x in let m,b = y in (¬(n = m ∈ ℤ)) ∨ p-sep(a;b)`

Lemma: pa-sep_wf
`∀[p:{2...}]. ∀[x,y:basic-padic(p)].  (pa-sep(p;x;y) ∈ ℙ)`

Lemma: pa-sep-or
`∀[p:{2...}]. ∀x,y:basic-padic(p).  (pa-sep(p;x;y) `` (∀z:basic-padic(p). (pa-sep(p;z;x) ∨ pa-sep(p;z;y))))`

Lemma: pa-sep-irrefl
`∀[p:{2...}]. ∀x:basic-padic(p). (¬pa-sep(p;x;x))`

Definition: pa-inv
`pa-inv(p;x) ==`
`  let n,a = x `
`  in if (n =z 0)`
`     then eval k = mu(λi.(¬b(a (i + 1) =z 0))) in`
`          let j,b = p-unitize(p;a;k + 1) `
`          in <j, p-inv(p;b)>`
`     else <0, p^n(p) * p-inv(p;a)>`
`     fi `

Lemma: pa-inv_wf
`∀p:{p:{2...}| prime(p)} . ∀x:{x:padic(p)| pa-sep(p;x;0(p))} .`
`  (pa-inv(p;x) ∈ {y:padic(p)| pa-mul(p;x;y) = 1(p) ∈ padic(p)} )`

Home Index