Library mathcomp.field.algnum
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ This file provides a few basic results and constructions in algebraic
+ number theory, that are used in the character theory library. Most of
+ these could be generalized to a more abstract setting. Note that the type
+ of abstract number fields is simply extFieldType rat. We define here:
+ x \in Crat_span X <=> x is a Q-linear combination of elements of
+ X : seq algC.
+ x \in Cint_span X <=> x is a Z-linear combination of elements of
+ X : seq algC.
+ x \in Aint <=> x : algC is an algebraic integer, i.e., the (monic)
+ polynomial of x over Q has integer coeficients.
+ (e %| a)%A <=> e divides a with respect to algebraic integers,
+ (e %| a)%Ax i.e., a is in the algebraic integer ideal generated
+ by e. This is is notation for a \in dvdA e, where
+ dvdv is the (collective) predicate for the Aint
+ ideal generated by e. As in the (e %| a)%C notation
+ e and a can be coerced to algC from nat or int.
+ The (e %| a)%Ax display form is a workaround for
+ design limitations of the Coq Notation facilities.
+ (a == b % [mod e])%A, (a != b % [mod e])%A <=>
+ a is equal (resp. not equal) to b mod e, i.e., a and
+ b belong to the same e * Aint class. We do not
+ force a, b and e to be algebraic integers.
+ # [x]%C == the multiplicative order of x, i.e., the n such that
+ x is an nth primitive root of unity, or 0 if x is not
+ a root of unity.
+ In addition several lemmas prove the (constructive) existence of number
+ fields and of automorphisms of algC.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GRing.Theory Num.Theory.
+Local Open Scope ring_scope.
+ +
+ +
+ +
+Local Hint Resolve (@intr_inj _ : injective ZtoC).
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GRing.Theory Num.Theory.
+Local Open Scope ring_scope.
+ +
+ +
+ +
+Local Hint Resolve (@intr_inj _ : injective ZtoC).
+ +
+
+ Number fields and rational spans.
+
+
+Lemma algC_PET (s : seq algC) :
+ {z | ∃ a : nat ^ size s, z = \sum_(i < size s) s`_i *+ a i
+ & ∃ ps, s = [seq (pQtoC p).[z] | p <- ps]}.
+ +
+Canonical subfx_unitAlgType (F L : fieldType) iota (z : L) p :=
+ Eval hnf in [unitAlgType F of subFExtend iota z p].
+ +
+Lemma num_field_exists (s : seq algC) :
+ {Qs : fieldExtType rat & {QsC : {rmorphism Qs → algC}
+ & {s1 : seq Qs | map QsC s1 = s & <<1 & s1>>%VS = fullv}}}.
+ +
+Definition in_Crat_span s x :=
+ ∃ a : rat ^ size s, x = \sum_i QtoC (a i) × s`_i.
+ +
+Fact Crat_span_subproof s x : decidable (in_Crat_span s x).
+ +
+Definition Crat_span s : pred algC := Crat_span_subproof s.
+Lemma Crat_spanP s x : reflect (in_Crat_span s x) (x \in Crat_span s).
+ Fact Crat_span_key s : pred_key (Crat_span s).
+Canonical Crat_span_keyed s := KeyedPred (Crat_span_key s).
+ +
+Lemma mem_Crat_span s : {subset s ≤ Crat_span s}.
+ +
+Fact Crat_span_zmod_closed s : zmod_closed (Crat_span s).
+Canonical Crat_span_opprPred s := OpprPred (Crat_span_zmod_closed s).
+Canonical Crat_span_addrPred s := AddrPred (Crat_span_zmod_closed s).
+Canonical Crat_span_zmodPred s := ZmodPred (Crat_span_zmod_closed s).
+ +
+Section MoreAlgCaut.
+ +
+Implicit Type rR : unitRingType.
+ +
+Lemma alg_num_field (Qz : fieldExtType rat) a : a%:A = ratr a :> Qz.
+ +
+Lemma rmorphZ_num (Qz : fieldExtType rat) rR (f : {rmorphism Qz → rR}) a x :
+ f (a *: x) = ratr a × f x.
+ +
+Lemma fmorph_numZ (Qz1 Qz2 : fieldExtType rat) (f : {rmorphism Qz1 → Qz2}) :
+ scalable f.
+ Definition NumLRmorphism Qz1 Qz2 f := AddLRMorphism (@fmorph_numZ Qz1 Qz2 f).
+ +
+End MoreAlgCaut.
+ +
+Section NumFieldProj.
+ +
+Variables (Qn : fieldExtType rat) (QnC : {rmorphism Qn → algC}).
+ +
+Lemma Crat_spanZ b a : {in Crat_span b, ∀ x, ratr a × x \in Crat_span b}.
+ +
+Lemma Crat_spanM b : {in Crat & Crat_span b, ∀ a x, a × x \in Crat_span b}.
+ +
+
+
++ {z | ∃ a : nat ^ size s, z = \sum_(i < size s) s`_i *+ a i
+ & ∃ ps, s = [seq (pQtoC p).[z] | p <- ps]}.
+ +
+Canonical subfx_unitAlgType (F L : fieldType) iota (z : L) p :=
+ Eval hnf in [unitAlgType F of subFExtend iota z p].
+ +
+Lemma num_field_exists (s : seq algC) :
+ {Qs : fieldExtType rat & {QsC : {rmorphism Qs → algC}
+ & {s1 : seq Qs | map QsC s1 = s & <<1 & s1>>%VS = fullv}}}.
+ +
+Definition in_Crat_span s x :=
+ ∃ a : rat ^ size s, x = \sum_i QtoC (a i) × s`_i.
+ +
+Fact Crat_span_subproof s x : decidable (in_Crat_span s x).
+ +
+Definition Crat_span s : pred algC := Crat_span_subproof s.
+Lemma Crat_spanP s x : reflect (in_Crat_span s x) (x \in Crat_span s).
+ Fact Crat_span_key s : pred_key (Crat_span s).
+Canonical Crat_span_keyed s := KeyedPred (Crat_span_key s).
+ +
+Lemma mem_Crat_span s : {subset s ≤ Crat_span s}.
+ +
+Fact Crat_span_zmod_closed s : zmod_closed (Crat_span s).
+Canonical Crat_span_opprPred s := OpprPred (Crat_span_zmod_closed s).
+Canonical Crat_span_addrPred s := AddrPred (Crat_span_zmod_closed s).
+Canonical Crat_span_zmodPred s := ZmodPred (Crat_span_zmod_closed s).
+ +
+Section MoreAlgCaut.
+ +
+Implicit Type rR : unitRingType.
+ +
+Lemma alg_num_field (Qz : fieldExtType rat) a : a%:A = ratr a :> Qz.
+ +
+Lemma rmorphZ_num (Qz : fieldExtType rat) rR (f : {rmorphism Qz → rR}) a x :
+ f (a *: x) = ratr a × f x.
+ +
+Lemma fmorph_numZ (Qz1 Qz2 : fieldExtType rat) (f : {rmorphism Qz1 → Qz2}) :
+ scalable f.
+ Definition NumLRmorphism Qz1 Qz2 f := AddLRMorphism (@fmorph_numZ Qz1 Qz2 f).
+ +
+End MoreAlgCaut.
+ +
+Section NumFieldProj.
+ +
+Variables (Qn : fieldExtType rat) (QnC : {rmorphism Qn → algC}).
+ +
+Lemma Crat_spanZ b a : {in Crat_span b, ∀ x, ratr a × x \in Crat_span b}.
+ +
+Lemma Crat_spanM b : {in Crat & Crat_span b, ∀ a x, a × x \in Crat_span b}.
+ +
+
+ In principle CtoQn could be taken to be additive and Q-linear, but this
+ would require a limit construction.
+
+
+Lemma num_field_proj : {CtoQn | CtoQn 0 = 0 & cancel QnC CtoQn}.
+ +
+Lemma restrict_aut_to_num_field (nu : {rmorphism algC → algC}) :
+ (∀ x, ∃ y, nu (QnC x) = QnC y) →
+ {nu0 : {lrmorphism Qn → Qn} | {morph QnC : x / nu0 x >-> nu x}}.
+ +
+Lemma map_Qnum_poly (nu : {rmorphism algC → algC}) p :
+ p \in polyOver 1%VS → map_poly (nu \o QnC) p = (map_poly QnC p).
+ +
+End NumFieldProj.
+ +
+Lemma restrict_aut_to_normal_num_field (Qn : splittingFieldType rat)
+ (QnC : {rmorphism Qn → algC})(nu : {rmorphism algC → algC}) :
+ {nu0 : {lrmorphism Qn → Qn} | {morph QnC : x / nu0 x >-> nu x}}.
+ +
+
+
++ +
+Lemma restrict_aut_to_num_field (nu : {rmorphism algC → algC}) :
+ (∀ x, ∃ y, nu (QnC x) = QnC y) →
+ {nu0 : {lrmorphism Qn → Qn} | {morph QnC : x / nu0 x >-> nu x}}.
+ +
+Lemma map_Qnum_poly (nu : {rmorphism algC → algC}) p :
+ p \in polyOver 1%VS → map_poly (nu \o QnC) p = (map_poly QnC p).
+ +
+End NumFieldProj.
+ +
+Lemma restrict_aut_to_normal_num_field (Qn : splittingFieldType rat)
+ (QnC : {rmorphism Qn → algC})(nu : {rmorphism algC → algC}) :
+ {nu0 : {lrmorphism Qn → Qn} | {morph QnC : x / nu0 x >-> nu x}}.
+ +
+
+ Integral spans.
+
+
+
+
+Lemma dec_Cint_span (V : vectType algC) m (s : m.-tuple V) v :
+ decidable (inIntSpan s v).
+ +
+Definition Cint_span (s : seq algC) : pred algC :=
+ fun x ⇒ dec_Cint_span (in_tuple [seq \row_(i < 1) y | y <- s]) (\row_i x).
+Fact Cint_span_key s : pred_key (Cint_span s).
+Canonical Cint_span_keyed s := KeyedPred (Cint_span_key s).
+ +
+Lemma Cint_spanP n (s : n.-tuple algC) x :
+ reflect (inIntSpan s x) (x \in Cint_span s).
+ +
+Lemma mem_Cint_span s : {subset s ≤ Cint_span s}.
+ +
+Lemma Cint_span_zmod_closed s : zmod_closed (Cint_span s).
+Canonical Cint_span_opprPred s := OpprPred (Cint_span_zmod_closed s).
+Canonical Cint_span_addrPred s := AddrPred (Cint_span_zmod_closed s).
+Canonical Cint_span_zmodPred s := ZmodPred (Cint_span_zmod_closed s).
+ +
+
+
++Lemma dec_Cint_span (V : vectType algC) m (s : m.-tuple V) v :
+ decidable (inIntSpan s v).
+ +
+Definition Cint_span (s : seq algC) : pred algC :=
+ fun x ⇒ dec_Cint_span (in_tuple [seq \row_(i < 1) y | y <- s]) (\row_i x).
+Fact Cint_span_key s : pred_key (Cint_span s).
+Canonical Cint_span_keyed s := KeyedPred (Cint_span_key s).
+ +
+Lemma Cint_spanP n (s : n.-tuple algC) x :
+ reflect (inIntSpan s x) (x \in Cint_span s).
+ +
+Lemma mem_Cint_span s : {subset s ≤ Cint_span s}.
+ +
+Lemma Cint_span_zmod_closed s : zmod_closed (Cint_span s).
+Canonical Cint_span_opprPred s := OpprPred (Cint_span_zmod_closed s).
+Canonical Cint_span_addrPred s := AddrPred (Cint_span_zmod_closed s).
+Canonical Cint_span_zmodPred s := ZmodPred (Cint_span_zmod_closed s).
+ +
+
+ Automorphism extensions.
+
+
+Lemma extend_algC_subfield_aut (Qs : fieldExtType rat)
+ (QsC : {rmorphism Qs → algC}) (phi : {rmorphism Qs → Qs}) :
+ {nu : {rmorphism algC → algC} | {morph QsC : x / phi x >-> nu x}}.
+ +
+
+
++ (QsC : {rmorphism Qs → algC}) (phi : {rmorphism Qs → Qs}) :
+ {nu : {rmorphism algC → algC} | {morph QsC : x / phi x >-> nu x}}.
+ +
+
+ Extended automorphisms of Q_n.
+
+
+Lemma Qn_aut_exists k n :
+ coprime k n →
+ {u : {rmorphism algC → algC} | ∀ z, z ^+ n = 1 → u z = z ^+ k}.
+ +
+
+
++ coprime k n →
+ {u : {rmorphism algC → algC} | ∀ z, z ^+ n = 1 → u z = z ^+ k}.
+ +
+
+ Algebraic integers.
+
+
+
+
+Definition Aint : pred_class :=
+ fun x : algC ⇒ minCpoly x \is a polyOver Cint.
+Fact Aint_key : pred_key Aint.
+Canonical Aint_keyed := KeyedPred Aint_key.
+ +
+Lemma root_monic_Aint p x :
+ root p x → p \is monic → p \is a polyOver Cint → x \in Aint.
+ +
+Lemma Cint_rat_Aint z : z \in Crat → z \in Aint → z \in Cint.
+ +
+Lemma Aint_Cint : {subset Cint ≤ Aint}.
+ +
+Lemma Aint_int x : x%:~R \in Aint.
+ +
+Lemma Aint0 : 0 \in Aint.
+Lemma Aint1 : 1 \in Aint.
+Hint Resolve Aint0 Aint1.
+ +
+Lemma Aint_unity_root n x : (n > 0)%N → n.-unity_root x → x \in Aint.
+ +
+Lemma Aint_prim_root n z : n.-primitive_root z → z \in Aint.
+ +
+Lemma Aint_Cnat : {subset Cnat ≤ Aint}.
+ +
+
+
++Definition Aint : pred_class :=
+ fun x : algC ⇒ minCpoly x \is a polyOver Cint.
+Fact Aint_key : pred_key Aint.
+Canonical Aint_keyed := KeyedPred Aint_key.
+ +
+Lemma root_monic_Aint p x :
+ root p x → p \is monic → p \is a polyOver Cint → x \in Aint.
+ +
+Lemma Cint_rat_Aint z : z \in Crat → z \in Aint → z \in Cint.
+ +
+Lemma Aint_Cint : {subset Cint ≤ Aint}.
+ +
+Lemma Aint_int x : x%:~R \in Aint.
+ +
+Lemma Aint0 : 0 \in Aint.
+Lemma Aint1 : 1 \in Aint.
+Hint Resolve Aint0 Aint1.
+ +
+Lemma Aint_unity_root n x : (n > 0)%N → n.-unity_root x → x \in Aint.
+ +
+Lemma Aint_prim_root n z : n.-primitive_root z → z \in Aint.
+ +
+Lemma Aint_Cnat : {subset Cnat ≤ Aint}.
+ +
+
+ This is Isaacs, Lemma (3.3)
+
+
+Lemma Aint_subring_exists (X : seq algC) :
+ {subset X ≤ Aint} →
+ {S : pred algC &
+ (*a*) subring_closed S
+ ∧ (*b*) {subset X ≤ S}
+ & (*c*) {Y : {n : nat & n.-tuple algC} &
+ {subset tagged Y ≤ S}
+ & ∀ x, reflect (inIntSpan (tagged Y) x) (x \in S)}}.
+ +
+Section AlgIntSubring.
+ +
+Import DefaultKeying GRing.DefaultPred perm.
+ +
+
+
++ {subset X ≤ Aint} →
+ {S : pred algC &
+ (*a*) subring_closed S
+ ∧ (*b*) {subset X ≤ S}
+ & (*c*) {Y : {n : nat & n.-tuple algC} &
+ {subset tagged Y ≤ S}
+ & ∀ x, reflect (inIntSpan (tagged Y) x) (x \in S)}}.
+ +
+Section AlgIntSubring.
+ +
+Import DefaultKeying GRing.DefaultPred perm.
+ +
+
+ This is Isaacs, Theorem (3.4).
+
+
+Theorem fin_Csubring_Aint S n (Y : n.-tuple algC) :
+ mulr_closed S → (∀ x, reflect (inIntSpan Y x) (x \in S)) →
+ {subset S ≤ Aint}.
+ +
+
+
++ mulr_closed S → (∀ x, reflect (inIntSpan Y x) (x \in S)) →
+ {subset S ≤ Aint}.
+ +
+
+ This is Isaacs, Corollary (3.5).
+
+
+Corollary Aint_subring : subring_closed Aint.
+Canonical Aint_opprPred := OpprPred Aint_subring.
+Canonical Aint_addrPred := AddrPred Aint_subring.
+Canonical Aint_mulrPred := MulrPred Aint_subring.
+Canonical Aint_zmodPred := ZmodPred Aint_subring.
+Canonical Aint_semiringPred := SemiringPred Aint_subring.
+Canonical Aint_smulrPred := SmulrPred Aint_subring.
+Canonical Aint_subringPred := SubringPred Aint_subring.
+ +
+End AlgIntSubring.
+ +
+Lemma Aint_aut (nu : {rmorphism algC → algC}) x :
+ (nu x \in Aint) = (x \in Aint).
+ +
+Definition dvdA (e : Algebraics.divisor) : pred_class :=
+ fun z : algC ⇒ if e == 0 then z == 0 else z / e \in Aint.
+Fact dvdA_key e : pred_key (dvdA e).
+Canonical dvdA_keyed e := KeyedPred (dvdA_key e).
+Delimit Scope algC_scope with A.
+Delimit Scope algC_expanded_scope with Ax.
+Notation "e %| x" := (x \in dvdA e) : algC_expanded_scope.
+Notation "e %| x" := (@in_mem Algebraics.divisor x (mem (dvdA e))) : algC_scope.
+ +
+Fact dvdA_zmod_closed e : zmod_closed (dvdA e).
+Canonical dvdA_opprPred e := OpprPred (dvdA_zmod_closed e).
+Canonical dvdA_addrPred e := AddrPred (dvdA_zmod_closed e).
+Canonical dvdA_zmodPred e := ZmodPred (dvdA_zmod_closed e).
+ +
+Definition eqAmod (e x y : Algebraics.divisor) := (e %| x - y)%A.
+Notation "x == y %[mod e ]" := (eqAmod e x y) : algC_scope.
+Notation "x != y %[mod e ]" := (~~ (eqAmod e x y)) : algC_scope.
+ +
+Lemma eqAmod_refl e x : (x == x %[mod e])%A.
+ Hint Resolve eqAmod_refl.
+ +
+Lemma eqAmod_sym e x y : ((x == y %[mod e]) = (y == x %[mod e]))%A.
+ +
+Lemma eqAmod_trans e y x z :
+ (x == y %[mod e] → y == z %[mod e] → x == z %[mod e])%A.
+ +
+Lemma eqAmod_transl e x y z :
+ (x == y %[mod e])%A → (x == z %[mod e])%A = (y == z %[mod e])%A.
+ +
+Lemma eqAmod_transr e x y z :
+ (x == y %[mod e])%A → (z == x %[mod e])%A = (z == y %[mod e])%A.
+ +
+Lemma eqAmod0 e x : (x == 0 %[mod e])%A = (e %| x)%A.
+ +
+Lemma eqAmodN e x y : (- x == y %[mod e])%A = (x == - y %[mod e])%A.
+ +
+Lemma eqAmodDr e x y z : (y + x == z + x %[mod e])%A = (y == z %[mod e])%A.
+ +
+Lemma eqAmodDl e x y z : (x + y == x + z %[mod e])%A = (y == z %[mod e])%A.
+ +
+Lemma eqAmodD e x1 x2 y1 y2 :
+ (x1 == x2 %[mod e] → y1 == y2 %[mod e] → x1 + y1 == x2 + y2 %[mod e])%A.
+ +
+Lemma eqAmodm0 e : (e == 0 %[mod e])%A.
+ Hint Resolve eqAmodm0.
+ +
+Lemma eqAmodMr e :
+ {in Aint, ∀ z x y, x == y %[mod e] → x × z == y × z %[mod e]}%A.
+ +
+Lemma eqAmodMl e :
+ {in Aint, ∀ z x y, x == y %[mod e] → z × x == z × y %[mod e]}%A.
+ +
+Lemma eqAmodMl0 e : {in Aint, ∀ x, x × e == 0 %[mod e]}%A.
+ +
+Lemma eqAmodMr0 e : {in Aint, ∀ x, e × x == 0 %[mod e]}%A.
+ +
+Lemma eqAmod_addl_mul e : {in Aint, ∀ x y, x × e + y == y %[mod e]}%A.
+ +
+Lemma eqAmodM e : {in Aint &, ∀ x1 y2 x2 y1,
+ x1 == x2 %[mod e] → y1 == y2 %[mod e] → x1 × y1 == x2 × y2 %[mod e]}%A.
+ +
+Lemma eqAmod_rat :
+ {in Crat & &, ∀ e m n, (m == n %[mod e])%A = (m == n %[mod e])%C}.
+ +
+Lemma eqAmod0_rat : {in Crat &, ∀ e n, (n == 0 %[mod e])%A = (e %| n)%C}.
+ +
+Lemma eqAmod_nat (e m n : nat) : (m == n %[mod e])%A = (m == n %[mod e])%N.
+ +
+Lemma eqAmod0_nat (e m : nat) : (m == 0 %[mod e])%A = (e %| m)%N.
+ +
+
+
++Canonical Aint_opprPred := OpprPred Aint_subring.
+Canonical Aint_addrPred := AddrPred Aint_subring.
+Canonical Aint_mulrPred := MulrPred Aint_subring.
+Canonical Aint_zmodPred := ZmodPred Aint_subring.
+Canonical Aint_semiringPred := SemiringPred Aint_subring.
+Canonical Aint_smulrPred := SmulrPred Aint_subring.
+Canonical Aint_subringPred := SubringPred Aint_subring.
+ +
+End AlgIntSubring.
+ +
+Lemma Aint_aut (nu : {rmorphism algC → algC}) x :
+ (nu x \in Aint) = (x \in Aint).
+ +
+Definition dvdA (e : Algebraics.divisor) : pred_class :=
+ fun z : algC ⇒ if e == 0 then z == 0 else z / e \in Aint.
+Fact dvdA_key e : pred_key (dvdA e).
+Canonical dvdA_keyed e := KeyedPred (dvdA_key e).
+Delimit Scope algC_scope with A.
+Delimit Scope algC_expanded_scope with Ax.
+Notation "e %| x" := (x \in dvdA e) : algC_expanded_scope.
+Notation "e %| x" := (@in_mem Algebraics.divisor x (mem (dvdA e))) : algC_scope.
+ +
+Fact dvdA_zmod_closed e : zmod_closed (dvdA e).
+Canonical dvdA_opprPred e := OpprPred (dvdA_zmod_closed e).
+Canonical dvdA_addrPred e := AddrPred (dvdA_zmod_closed e).
+Canonical dvdA_zmodPred e := ZmodPred (dvdA_zmod_closed e).
+ +
+Definition eqAmod (e x y : Algebraics.divisor) := (e %| x - y)%A.
+Notation "x == y %[mod e ]" := (eqAmod e x y) : algC_scope.
+Notation "x != y %[mod e ]" := (~~ (eqAmod e x y)) : algC_scope.
+ +
+Lemma eqAmod_refl e x : (x == x %[mod e])%A.
+ Hint Resolve eqAmod_refl.
+ +
+Lemma eqAmod_sym e x y : ((x == y %[mod e]) = (y == x %[mod e]))%A.
+ +
+Lemma eqAmod_trans e y x z :
+ (x == y %[mod e] → y == z %[mod e] → x == z %[mod e])%A.
+ +
+Lemma eqAmod_transl e x y z :
+ (x == y %[mod e])%A → (x == z %[mod e])%A = (y == z %[mod e])%A.
+ +
+Lemma eqAmod_transr e x y z :
+ (x == y %[mod e])%A → (z == x %[mod e])%A = (z == y %[mod e])%A.
+ +
+Lemma eqAmod0 e x : (x == 0 %[mod e])%A = (e %| x)%A.
+ +
+Lemma eqAmodN e x y : (- x == y %[mod e])%A = (x == - y %[mod e])%A.
+ +
+Lemma eqAmodDr e x y z : (y + x == z + x %[mod e])%A = (y == z %[mod e])%A.
+ +
+Lemma eqAmodDl e x y z : (x + y == x + z %[mod e])%A = (y == z %[mod e])%A.
+ +
+Lemma eqAmodD e x1 x2 y1 y2 :
+ (x1 == x2 %[mod e] → y1 == y2 %[mod e] → x1 + y1 == x2 + y2 %[mod e])%A.
+ +
+Lemma eqAmodm0 e : (e == 0 %[mod e])%A.
+ Hint Resolve eqAmodm0.
+ +
+Lemma eqAmodMr e :
+ {in Aint, ∀ z x y, x == y %[mod e] → x × z == y × z %[mod e]}%A.
+ +
+Lemma eqAmodMl e :
+ {in Aint, ∀ z x y, x == y %[mod e] → z × x == z × y %[mod e]}%A.
+ +
+Lemma eqAmodMl0 e : {in Aint, ∀ x, x × e == 0 %[mod e]}%A.
+ +
+Lemma eqAmodMr0 e : {in Aint, ∀ x, e × x == 0 %[mod e]}%A.
+ +
+Lemma eqAmod_addl_mul e : {in Aint, ∀ x y, x × e + y == y %[mod e]}%A.
+ +
+Lemma eqAmodM e : {in Aint &, ∀ x1 y2 x2 y1,
+ x1 == x2 %[mod e] → y1 == y2 %[mod e] → x1 × y1 == x2 × y2 %[mod e]}%A.
+ +
+Lemma eqAmod_rat :
+ {in Crat & &, ∀ e m n, (m == n %[mod e])%A = (m == n %[mod e])%C}.
+ +
+Lemma eqAmod0_rat : {in Crat &, ∀ e n, (n == 0 %[mod e])%A = (e %| n)%C}.
+ +
+Lemma eqAmod_nat (e m n : nat) : (m == n %[mod e])%A = (m == n %[mod e])%N.
+ +
+Lemma eqAmod0_nat (e m : nat) : (m == 0 %[mod e])%A = (e %| m)%N.
+ +
+
+ Multiplicative order.
+
+
+