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)
Definition: add_grp_of_rng
r↓+gp == <|r|, =b, ≤b, +r, 0, -r>
Lemma: add_grp_of_rng_wf
∀[r:RngSig]. (r↓+gp ∈ GrpSig)
Lemma: add_grp_of_rng_wf_a
∀[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)
Lemma: add_grp_of_rng_wf_b
∀[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|)
Lemma: rng_nat_op_add
∀[r:Rng]. ∀[e:|r|]. ∀[a,b:ℕ]. (((a + b) ⋅r e) = ((a ⋅r e) +r (b ⋅r e)) ∈ |r|)
Lemma: int-to-ring-add
∀[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|)
Lemma: ring_term_value_add_lemma
∀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
Lemma: itermAdd_functionality_wrt_ringeq
∀[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|)
Lemma: imonomial-term-add-ringeq
∀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)
Lemma: add-ipoly-ringeq
∀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|)
Definition: p-adics
p-adics(p) == {f:n:ℕ+ ⟶ ℕp^n| ∀n:ℕ+. ((f (n + 1)) ≡ (f n) mod p^n)}
Lemma: p-adics_wf
∀[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)
Definition: p-add
x + y == λn.(x n) + (y n) mod(p^n)
Lemma: p-add_wf
∀[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))
Lemma: p-adics-subtype
∀[p:ℕ+]. (p-adics(p) ⊆r (ℕ+ ⟶ ℤ))
Lemma: equal-p-adics
∀[p:ℕ+]. ∀[x,y:p-adics(p)]. uiff(x = y ∈ p-adics(p);x = y ∈ (ℕ+ ⟶ ℤ))
Lemma: p-adics-equal
∀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))
Lemma: p-add-int
∀[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))
Lemma: p-adic-property
∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+. ∀m:{n...}. ((a m) ≡ (a n) mod p^n)
Lemma: p-adic-bounds
∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+. ((0 ≤ ((a (n + 1)) - a n)) ∧ (((a (n + 1)) - a n) ≤ (p^(n + 1) - p^n)))
Lemma: p-adic-non-decreasing
∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+. ∀i:ℕ+n + 1. ((a i) ≤ (a n))
Lemma: p-adic-inv-lemma1
∀p:{p:{2...}| prime(p)} . ∀a:{a:p-adics(p)| ¬((a 1) = 0 ∈ ℤ)} . ∀n:ℕ+. (∃c:ℕp^n [((c * (a n)) ≡ 1 mod p^n)])
Lemma: p-adic-inv-lemma
∀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)} )
Definition: p-adic-ring
ℤ(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 ⋅ )>
Lemma: p-adic-ring_wf
∀[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))
Lemma: p-add-assoc
∀[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))
Lemma: int-ring-hom-p-adic-ring
∀[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)))
Definition: basic-padic
basic-padic(p) == ℕ × p-adics(p)
Lemma: basic-padic_wf
∀[p:ℤ]. (basic-padic(p) ∈ Type)
Definition: bpa-add
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>
Lemma: bpa-add_wf
∀[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))
Definition: padic
padic(p) == n:ℕ × if (n =z 0) then p-adics(p) else p-units(p) fi
Lemma: padic_wf
∀[p:ℤ]. (padic(p) ∈ Type)
Lemma: padic_subtype_basic-padic
∀[p:ℤ]. (padic(p) ⊆r basic-padic(p))
Lemma: bpa-norm_wf_padic
∀[p:ℕ+]. ∀[x:basic-padic(p)]. (bpa-norm(p;x) ∈ padic(p))
Lemma: equal-padics
∀[p:ℤ]. ∀[x,y:padic(p)]. uiff(x = y ∈ padic(p);x = y ∈ basic-padic(p))
Lemma: bpa-norm-padic
∀[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))
Definition: mkpadic
(a/p^n) == bpa-norm(p;<n, a>)
Lemma: mkpadic_wf
∀[p:ℕ+]. ∀[n:ℕ]. ∀[a:p-adics(p)]. ((a/p^n) ∈ padic(p))
Lemma: mkpadic_functionality
∀[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>)
Lemma: mkpadic-equiv
∀[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))
Definition: pa-add
pa-add(p;x;y) == bpa-norm(p;bpa-add(p;x;y))
Lemma: pa-add_wf
∀[p:{2...}]. ∀[x,y:basic-padic(p)]. (pa-add(p;x;y) ∈ padic(p))
Lemma: pa-add_functionality
∀[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))
Definition: padic-ring
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 ⋅ )>
Lemma: padic-ring_wf
∀[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