- -

Library mathcomp.field.algC

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- This file provides an axiomatic construction of the algebraic numbers. - The construction only assumes the existence of an algebraically closed - filed with an automorphism of order 2; this amounts to the purely - algebraic contents of the Fundamenta Theorem of Algebra. - algC == the closed, countable field of algebraic numbers. - algCeq, algCring, ..., algCnumField == structures for algC. - The ssrnum interfaces are implemented for algC as follows: - x <= y <=> (y - x) is a nonnegative real - x < y <=> (y - x) is a (strictly) positive real - `|z| == the complex norm of z, i.e., sqrtC (z * z^* ). - Creal == the subset of real numbers (:= Num.real for algC). - 'i == the imaginary number (:= sqrtC (-1)). - 'Re z == the real component of z. - 'Im z == the imaginary component of z. - z^* == the complex conjugate of z (:= conjC z). - sqrtC z == a nonnegative square root of z, i.e., 0 <= sqrt x if 0 <= x. - n.-root z == more generally, for n > 0, an nth root of z, chosen with a - minimal non-negative argument for n > 1 (i.e., with a - maximal real part subject to a nonnegative imaginary part). - Note that n.-root (-1) is a primitive 2nth root of unity, - an thus not equal to -1 for n odd > 1 (this will be shown in - file cyclotomic.v). - In addition, we provide: - Crat == the subset of rational numbers. - Cint == the subset of integers. - Cnat == the subset of natural integers. - getCrat z == some a : rat such that ratr a = z, provided z \in Crat. - floorC z == for z \in Creal, an m : int s.t. m%:~R <= z < (m + 1)%:~R. - truncC z == for z >= 0, an n : nat s.t. n%:R <= z < n.+1%:R, else 0%N. - minCpoly z == the minimal (monic) polynomial over Crat with root z. - algC_invaut nu == an inverse of nu : {rmorphism algC -> algC}. - (x %| y)%C <=> y is an integer (Cint) multiple of x; if x or y are - (x %| y)%Cx of type nat or int they are coerced to algC here. - The (x %| y)%Cx display form is a workaround for - design limitations of the Coq Notation facilities. - (x == y % [mod z])%C <=> x and y differ by an integer (Cint) multiple of z; - as above, arguments of type nat or int are cast to algC. - (x != y % [mod z])%C <=> x and y do not differ by an integer multiple of z. - Note that in file algnum we give an alternative definition of divisibility - based on algebraic integers, overloading the notation in the %A scope. -

- -
-Set Implicit Arguments.
- -
-Import GRing.Theory Num.Theory.
-Local Open Scope ring_scope.
- -
-

- -

- The Num mixin for an algebraically closed field with an automorphism of - order 2, making it into a field of complex numbers. -

-Lemma ComplexNumMixin (L : closedFieldType) (conj : {rmorphism L → L }) :
-    involutive conj → ¬ conj =1 id →
-  {numL | ∀ x : NumDomainType L numL, `|x | ^+ 2 = x × conj x }.
- -
-Module Algebraics.
- -
-Module Type Specification.
- -
-Parameter type : Type.
- -
-Parameter eqMixin : Equality.class_of type.
-Canonical eqType := EqType type eqMixin.
- -
-Parameter choiceMixin : Choice.mixin_of type.
-Canonical choiceType := ChoiceType type choiceMixin.
- -
-Parameter countMixin : Countable.mixin_of type.
-Canonical countType := CountType type countMixin.
- -
-Parameter zmodMixin : GRing.Zmodule.mixin_of type.
-Canonical zmodType := ZmodType type zmodMixin.
-Canonical countZmodType := [countZmodType of type ].
- -
-Parameter ringMixin : GRing.Ring.mixin_of zmodType.
-Canonical ringType := RingType type ringMixin.
-Canonical countRingType := [countRingType of type ].
- -
-Parameter unitRingMixin : GRing.UnitRing.mixin_of ringType.
-Canonical unitRingType := UnitRingType type unitRingMixin.
- -
-Axiom mulC : @commutative ringType ringType *%R.
-Canonical comRingType := ComRingType type mulC.
-Canonical comUnitRingType := [comUnitRingType of type ].
- -
-Axiom idomainAxiom : GRing.IntegralDomain.axiom ringType.
-Canonical idomainType := IdomainType type idomainAxiom.
- -
-Axiom fieldMixin : GRing.Field.mixin_of unitRingType.
-Canonical fieldType := FieldType type fieldMixin.
- -
-Parameter decFieldMixin : GRing.DecidableField.mixin_of unitRingType.
-Canonical decFieldType := DecFieldType type decFieldMixin.
- -
-Axiom closedFieldAxiom : GRing.ClosedField.axiom ringType.
-Canonical closedFieldType := ClosedFieldType type closedFieldAxiom.
- -
-Parameter numMixin : Num.mixin_of ringType.
-Canonical numDomainType := NumDomainType type numMixin.
-Canonical numFieldType := [numFieldType of type ].
- -
-Parameter conjMixin : Num.ClosedField.imaginary_mixin_of numDomainType.
-Canonical numClosedFieldType := NumClosedFieldType type conjMixin.
- -
-Axiom algebraic : integralRange (@ratr unitRingType).
- -
-End Specification.
- -
-Module Implementation : Specification.
- -
-Definition L := tag Fundamental_Theorem_of_Algebraics.
- -
-Definition conjL : {rmorphism L → L } :=
-  s2val (tagged Fundamental_Theorem_of_Algebraics).
- -
-Fact conjL_K : involutive conjL.
- -
-Fact conjL_nt : ¬ conjL =1 id.
- -
-Definition LnumMixin := ComplexNumMixin conjL_K conjL_nt.
-Definition Lnum := NumDomainType L (sval LnumMixin).
- -
-Definition QtoL := [rmorphism of @ratr [numFieldType of Lnum ]].
-Notation pQtoL := (map_poly QtoL).
- -
-Definition rootQtoL p_j :=
-  if p_j .1 == 0 then 0 else
-  (sval (closed_field_poly_normal (pQtoL p_j .1)))`_p_j .2.
- -
-Definition eq_root p_j q_k := rootQtoL p_j == rootQtoL q_k.
-Fact eq_root_is_equiv : equiv_class_of eq_root.
- Canonical eq_root_equiv := EquivRelPack eq_root_is_equiv.
-Definition type : Type := {eq_quot eq_root }%qT.
- -
-Definition eqMixin : Equality.class_of type := EquivQuot.eqMixin _.
-Canonical eqType := EqType type eqMixin.
- -
-Definition choiceMixin : Choice.mixin_of type := EquivQuot.choiceMixin _.
-Canonical choiceType := ChoiceType type choiceMixin.
- -
-Definition countMixin : Countable.mixin_of type := CanCountMixin reprK.
-Canonical countType := CountType type countMixin.
- -
-Definition CtoL (u : type) := rootQtoL (repr u).
- -
-Fact CtoL_inj : injective CtoL.
- -
-Fact CtoL_P u : integralOver QtoL (CtoL u).
- -
-Fact LtoC_subproof z : integralOver QtoL z → {u | CtoL u = z }.
- -
-Definition LtoC z Az := sval (@LtoC_subproof z Az).
-Fact LtoC_K z Az : CtoL (@LtoC z Az) = z.
- -
-Fact CtoL_K u : LtoC (CtoL_P u) = u.
- -
-Definition zero := LtoC (integral0 _).
-Definition add u v := LtoC (integral_add (CtoL_P u) (CtoL_P v)).
-Definition opp u := LtoC (integral_opp (CtoL_P u)).
- -
-Fact addA : associative add.
- -
-Fact addC : commutative add.
- -
-Fact add0 : left_id zero add.
- -
-Fact addN : left_inverse zero opp add.
- -
-Definition zmodMixin := ZmodMixin addA addC add0 addN.
-Canonical zmodType := ZmodType type zmodMixin.
-Canonical countZmodType := [countZmodType of type ].
- -
-Fact CtoL_is_additive : additive CtoL.
- Canonical CtoL_additive := Additive CtoL_is_additive.
- -
-Definition one := LtoC (integral1 _).
-Definition mul u v := LtoC (integral_mul (CtoL_P u) (CtoL_P v)).
-Definition inv u := LtoC (integral_inv (CtoL_P u)).
- -
-Fact mulA : associative mul.
- -
-Fact mulC : commutative mul.
- -
-Fact mul1 : left_id one mul.
- -
-Fact mulD : left_distributive mul +%R.
- -
-Fact one_nz : one != 0 :> type.
- -
-Definition ringMixin := ComRingMixin mulA mulC mul1 mulD one_nz.
-Canonical ringType := RingType type ringMixin.
-Canonical comRingType := ComRingType type mulC.
-Canonical countRingType := [countRingType of type ].
- -
-Fact CtoL_is_multiplicative : multiplicative CtoL.
- Canonical CtoL_rmorphism := AddRMorphism CtoL_is_multiplicative.
- -
-Fact mulVf : GRing.Field.axiom inv.
-Fact inv0 : inv 0 = 0.
- -
-Definition unitRingMixin := FieldUnitMixin mulVf inv0.
-Canonical unitRingType := UnitRingType type unitRingMixin.
-Canonical comUnitRingType := [comUnitRingType of type ].
- -
-Definition fieldMixin := FieldMixin mulVf inv0.
-Definition idomainAxiom := FieldIdomainMixin fieldMixin.
-Canonical idomainType := IdomainType type idomainAxiom.
-Canonical fieldType := FieldType type fieldMixin.
- -
-Fact closedFieldAxiom : GRing.ClosedField.axiom ringType.
- -
-Definition decFieldMixin := closed_field_QEMixin closedFieldAxiom.
-Canonical decFieldType := DecFieldType type decFieldMixin.
-Canonical closedFieldType := ClosedFieldType type closedFieldAxiom.
- -
-Fact conj_subproof u : integralOver QtoL (conjL (CtoL u)).
-Fact conj_is_rmorphism : rmorphism (fun u ⇒ LtoC (conj_subproof u)).
-Definition conj : {rmorphism type → type } := RMorphism conj_is_rmorphism.
-Lemma conjK : involutive conj.
- -
-Fact conj_nt : ¬ conj =1 id.
- -
-Definition numMixin := sval (ComplexNumMixin conjK conj_nt).
-Canonical numDomainType := NumDomainType type numMixin.
-Canonical numFieldType := [numFieldType of type ].
- -
-Lemma normK u : `|u | ^+ 2 = u × conj u.
- -
-Lemma algebraic : integralRange (@ratr unitRingType).
- -
-Definition conjMixin :=
-  ImaginaryMixin (svalP (imaginary_exists closedFieldType))
-                 (fun x ⇒ esym (normK x)).
-Canonical numClosedFieldType := NumClosedFieldType type conjMixin.
- -
-End Implementation.
- -
-Definition divisor := Implementation.type.
- -
-Module Internals.
- -
-Import Implementation.
- -
- -
-Fact algCi_subproof : {i : algC | i ^+ 2 = -1}.
- -
-Variant getCrat_spec : Type := GetCrat_spec CtoQ of cancel QtoC CtoQ.
- -
-Fact getCrat_subproof : getCrat_spec.
- -
-Fact floorC_subproof x : {m | x \is Creal → ZtoC m ≤ x < ZtoC (m + 1)}.
- -
-Fact minCpoly_subproof (x : algC) :
-  {p | p \is monic & ∀ q, root (pQtoC q) x = (p %| q)%R}.
- -
-Definition algC_divisor (x : algC) := x : divisor.
-Definition int_divisor m := m %:~R : divisor.
-Definition nat_divisor n := n %:R : divisor.
- -
-End Internals.
- -
-Module Import Exports.
- -
-Import Implementation Internals.
- -
-Notation algC := type.
-Delimit Scope C_scope with C.
-Delimit Scope C_core_scope with Cc.
-Delimit Scope C_expanded_scope with Cx.
-Open Scope C_core_scope.
- -
-Canonical eqType.
-Canonical choiceType.
-Canonical countType.
-Canonical zmodType.
-Canonical countZmodType.
-Canonical ringType.
-Canonical countRingType.
-Canonical unitRingType.
-Canonical comRingType.
-Canonical comUnitRingType.
-Canonical idomainType.
-Canonical numDomainType.
-Canonical fieldType.
-Canonical numFieldType.
-Canonical decFieldType.
-Canonical closedFieldType.
-Canonical numClosedFieldType.
- -
-Notation algCeq := eqType.
-Notation algCzmod := zmodType.
-Notation algCring := ringType.
-Notation algCuring := unitRingType.
-Notation algCnum := numDomainType.
-Notation algCfield := fieldType.
-Notation algCnumField := numFieldType.
-Notation algCnumClosedField := numClosedFieldType.
- -
-Notation Creal := (@Num.Def.Rreal numDomainType).
- -
-Definition getCrat := let: GetCrat_spec CtoQ _ := getCrat_subproof in CtoQ.
-Definition Crat : {pred algC } := fun x ⇒ ratr (getCrat x) == x.
- -
-Definition floorC x := sval (floorC_subproof x).
-Definition Cint : {pred algC } := fun x ⇒ (floorC x )%:~R == x.
- -
-Definition truncC x := if x ≥ 0 then `|floorC x |%N else 0%N.
-Definition Cnat : {pred algC } := fun x ⇒ (truncC x )%:R == x.
- -
-Definition minCpoly x : {poly algC } :=
-  let: exist2 p _ _ := minCpoly_subproof x in map_poly ratr p.
- -
-Coercion nat_divisor : nat >-> divisor.
-Coercion int_divisor : int >-> divisor.
-Coercion algC_divisor : algC >-> divisor.
- -
-Lemma nCdivE (p : nat) : p = p %:R :> divisor.
-Lemma zCdivE (p : int) : p = p %:~R :> divisor.
-Definition CdivE := (nCdivE , zCdivE ).
- -
-Definition dvdC (x : divisor) : {pred algC } :=
-   fun y ⇒ if x == 0 then y == 0 else y / x \in Cint.
-Notation "x %| y" := (y \in dvdC x) : C_expanded_scope.
-Notation "x %| y" := (@in_mem divisor y (mem (dvdC x))) : C_scope.
- -
-Definition eqCmod (e x y : divisor) := (e %| x - y)%C.
- -
-Notation "x == y %[mod e ]" := (eqCmod e x y) : C_scope.
-Notation "x != y %[mod e ]" := (~~ (x == y %[mod e])%C) : C_scope.
- -
-End Exports.
- -
-End Algebraics.
- -
-Export Algebraics.Exports.
- -
-Section AlgebraicsTheory.
- -
-Implicit Types (x y z : algC) (n : nat) (m : int) (b : bool).
-Import Algebraics.Internals.
- -
- -
-Local Hint Resolve (intr_inj : injective ZtoC) : core.
- -
-

- -

- Specialization of a few basic ssrnum order lemmas. -

- -
-Definition eqC_nat n p : (n %:R == p %:R :> algC ) = (n == p ) := eqr_nat _ n p.
-Definition leC_nat n p : (n %:R ≤ p %:R :> algC ) = (n ≤ p)%N := ler_nat _ n p.
-Definition ltC_nat n p : (n %:R < p %:R :> algC ) = (n < p)%N := ltr_nat _ n p.
-Definition Cchar : [char algC ] =i pred0 := @char_num _.
- -
-

- -

- This can be used in the converse direction to evaluate assertions over - manifest rationals, such as 3%:R^-1 + 7%:%^-1 < 2%:%^-1 :> algC. - Missing norm and integer exponent, due to gaps in ssrint and rat. -

-Definition CratrE :=
-  let CnF := Algebraics.Implementation.numFieldType in
-  let QtoCm := ratr_rmorphism CnF in
-  ((rmorph0 QtoCm , rmorph1 QtoCm , rmorphMn QtoCm , rmorphN QtoCm , rmorphD QtoCm ),
-   (rmorphM QtoCm , rmorphX QtoCm , fmorphV QtoCm ),
-   (rmorphMz QtoCm , rmorphXz QtoCm , @ratr_norm CnF , @ratr_sg CnF ),
-   =^~ (@ler_rat CnF , @ltr_rat CnF , (inj_eq (fmorph_inj QtoCm)))).
- -
-Definition CintrE :=
-  let CnF := Algebraics.Implementation.numFieldType in
-  let ZtoCm := intmul1_rmorphism CnF in
-  ((rmorph0 ZtoCm , rmorph1 ZtoCm , rmorphMn ZtoCm , rmorphN ZtoCm , rmorphD ZtoCm ),
-   (rmorphM ZtoCm , rmorphX ZtoCm ),
-   (rmorphMz ZtoCm , @intr_norm CnF , @intr_sg CnF ),
-   =^~ (@ler_int CnF , @ltr_int CnF , (inj_eq (@intr_inj CnF)))).
- -
-Let nz2 : 2%:R != 0 :> algC.
- -
-

- -

- Conjugation and norm. -

- -
-Definition algC_algebraic x := Algebraics.Implementation.algebraic x.
- -
-

- -

- Real number subset. -

- -
-Lemma Creal0 : 0 \is Creal.
-Lemma Creal1 : 1 \is Creal.
-

- -

- Trivial cannot resolve a general real0 hint. -

-Hint Resolve Creal0 Creal1 : core.
- -
-Lemma algCrect x : x = 'Re x + 'i × 'Im x.
- -
-Lemma algCreal_Re x : 'Re x \is Creal.
- -
-Lemma algCreal_Im x : 'Im x \is Creal.
- Hint Resolve algCreal_Re algCreal_Im : core.
- -
-

- -

- Integer subset. - Not relying on the undocumented interval library, for now. -

- -
-Lemma floorC_itv x : x \is Creal → (floorC x )%:~R ≤ x < (floorC x + 1)%:~R.
- -
-Lemma floorC_def x m : m %:~R ≤ x < (m + 1)%:~R → floorC x = m.
- -
-Lemma intCK : cancel intr floorC.
- -
-Lemma floorCK : {in Cint , cancel floorC intr }.
- -
-Lemma floorC0 : floorC 0 = 0.
-Lemma floorC1 : floorC 1 = 1.
-Hint Resolve floorC0 floorC1 : core.
- -
-Lemma floorCpK (p : {poly algC }) :
-  p \is a polyOver Cint → map_poly intr (map_poly floorC p) = p.
- -
-Lemma floorCpP (p : {poly algC }) :
-  p \is a polyOver Cint → {q | p = map_poly intr q }.
- -
-Lemma Cint_int m : m %:~R \in Cint.
- -
-Lemma CintP x : reflect (∃ m, x = m %:~R) (x \in Cint).
- -
-Lemma floorCD : {in Cint & Creal , {morph floorC : x y / x + y }}.
- -
-Lemma floorCN : {in Cint , {morph floorC : x / - x }}.
- -
-Lemma floorCM : {in Cint &, {morph floorC : x y / x × y }}.
- -
-Lemma floorCX n : {in Cint , {morph floorC : x / x ^+ n }}.
- -
-Lemma rpred_Cint
-        (S : {pred algC }) (ringS : subringPred S) (kS : keyed_pred ringS) x :
-  x \in Cint → x \in kS.
- -
-Lemma Cint0 : 0 \in Cint.
-Lemma Cint1 : 1 \in Cint.
-Hint Resolve Cint0 Cint1 : core.
- -
-Fact Cint_key : pred_key Cint.
-Fact Cint_subring : subring_closed Cint.
-Canonical Cint_keyed := KeyedPred Cint_key.
-Canonical Cint_opprPred := OpprPred Cint_subring.
-Canonical Cint_addrPred := AddrPred Cint_subring.
-Canonical Cint_mulrPred := MulrPred Cint_subring.
-Canonical Cint_zmodPred := ZmodPred Cint_subring.
-Canonical Cint_semiringPred := SemiringPred Cint_subring.
-Canonical Cint_smulrPred := SmulrPred Cint_subring.
-Canonical Cint_subringPred := SubringPred Cint_subring.
- -
-Lemma Creal_Cint : {subset Cint ≤ Creal }.
- -
-Lemma conj_Cint x : x \in Cint → x ^* = x.
- -
-Lemma Cint_normK x : x \in Cint → `|x | ^+ 2 = x ^+ 2.
- -
-Lemma CintEsign x : x \in Cint → x = (-1) ^+ (x < 0)%C × `|x |.
- -
-

- -

- Natural integer subset. -

- -
-Lemma truncC_itv x : 0 ≤ x → (truncC x )%:R ≤ x < (truncC x ).+1 %:R.
- -
-Lemma truncC_def x n : n %:R ≤ x < n .+1 %:R → truncC x = n.
- -
-Lemma natCK n : truncC n %:R = n.
- -
-Lemma CnatP x : reflect (∃ n, x = n %:R) (x \in Cnat).
- -
-Lemma truncCK : {in Cnat , cancel truncC (GRing.natmul 1)}.
- -
-Lemma truncC_gt0 x : (0 < truncC x)%N = (1 ≤ x ).
- -
-Lemma truncC0Pn x : reflect (truncC x = 0%N) (~~ (1 ≤ x )).
- -
-Lemma truncC0 : truncC 0 = 0%N.
-Lemma truncC1 : truncC 1 = 1%N.
- -
-Lemma truncCD :
-  {in Cnat & Num.nneg , {morph truncC : x y / x + y >-> (x + y)%N}}.
- -
-Lemma truncCM : {in Cnat &, {morph truncC : x y / x × y >-> (x × y)%N}}.
- -
-Lemma truncCX n : {in Cnat , {morph truncC : x / x ^+ n >-> (x ^ n)%N}}.
- -
-Lemma rpred_Cnat
-        (S : {pred algC }) (ringS : semiringPred S) (kS : keyed_pred ringS) x :
-  x \in Cnat → x \in kS.
- -
-Lemma Cnat_nat n : n %:R \in Cnat.
-Lemma Cnat0 : 0 \in Cnat.
-Lemma Cnat1 : 1 \in Cnat.
-Hint Resolve Cnat_nat Cnat0 Cnat1 : core.
- -
-Fact Cnat_key : pred_key Cnat.
-Fact Cnat_semiring : semiring_closed Cnat.
-Canonical Cnat_keyed := KeyedPred Cnat_key.
-Canonical Cnat_addrPred := AddrPred Cnat_semiring.
-Canonical Cnat_mulrPred := MulrPred Cnat_semiring.
-Canonical Cnat_semiringPred := SemiringPred Cnat_semiring.
- -
-Lemma Cnat_ge0 x : x \in Cnat → 0 ≤ x.
- -
-Lemma Cnat_gt0 x : x \in Cnat → (0 < x ) = (x != 0).
- -
-Lemma conj_Cnat x : x \in Cnat → x ^* = x.
- -
-Lemma norm_Cnat x : x \in Cnat → `|x | = x.
- -
-Lemma Creal_Cnat : {subset Cnat ≤ Creal }.
- -
-Lemma Cnat_sum_eq1 (I : finType) (P : pred I) (F : I → algC) :
-     (∀ i, P i → F i \in Cnat ) → \sum_(i | P i ) F i = 1 →
-   {i : I | [/\ P i , F i = 1 & ∀ j, j != i → P j → F j = 0]}.
- -
-Lemma Cnat_mul_eq1 x y :
-  x \in Cnat → y \in Cnat → (x × y == 1) = (x == 1) && (y == 1).
- -
-Lemma Cnat_prod_eq1 (I : finType) (P : pred I) (F : I → algC) :
-    (∀ i, P i → F i \in Cnat ) → \prod_(i | P i ) F i = 1 →
-  ∀ i, P i → F i = 1.
- -
-

- -

- Relating Cint and Cnat. -

- -
-Lemma Cint_Cnat : {subset Cnat ≤ Cint }.
- -
-Lemma CintE x : (x \in Cint ) = (x \in Cnat ) || (- x \in Cnat ).
- -
-Lemma Cnat_norm_Cint x : x \in Cint → `|x | \in Cnat.
- -
-Lemma CnatEint x : (x \in Cnat ) = (x \in Cint ) && (0 ≤ x ).
- -
-Lemma CintEge0 x : 0 ≤ x → (x \in Cint ) = (x \in Cnat ).
- -
-Lemma Cnat_exp_even x n : ~~ odd n → x \in Cint → x ^+ n \in Cnat.
- -
-Lemma norm_Cint_ge1 x : x \in Cint → x != 0 → 1 ≤ `|x |.
- -
-Lemma sqr_Cint_ge1 x : x \in Cint → x != 0 → 1 ≤ x ^+ 2.
- -
-Lemma Cint_ler_sqr x : x \in Cint → x ≤ x ^+ 2.
- -
-

- -

- Integer divisibility. -

- -
-Lemma dvdCP x y : reflect (exists2 z, z \in Cint & y = z × x) (x %| y)%C.
- -
-Lemma dvdCP_nat x y : 0 ≤ x → 0 ≤ y → (x %| y)%C → {n | y = n %:R × x }.
- -
-Lemma dvdC0 x : (x %| 0)%C.
- -
-Lemma dvd0C x : (0 %| x)%C = (x == 0).
- -
-Lemma dvdC_mull x y z : y \in Cint → (x %| z)%C → (x %| y × z)%C.
- -
-Lemma dvdC_mulr x y z : y \in Cint → (x %| z)%C → (x %| z × y)%C.
- -
-Lemma dvdC_mul2r x y z : y != 0 → (x × y %| z × y)%C = (x %| z)%C.
- -
-Lemma dvdC_mul2l x y z : y != 0 → (y × x %| y × z)%C = (x %| z)%C.
- -
-Lemma dvdC_trans x y z : (x %| y)%C → (y %| z)%C → (x %| z)%C.
- -
-Lemma dvdC_refl x : (x %| x)%C.
- Hint Resolve dvdC_refl : core.
- -
-Fact dvdC_key x : pred_key (dvdC x).
-Lemma dvdC_zmod x : zmod_closed (dvdC x).
-Canonical dvdC_keyed x := KeyedPred (dvdC_key x).
-Canonical dvdC_opprPred x := OpprPred (dvdC_zmod x).
-Canonical dvdC_addrPred x := AddrPred (dvdC_zmod x).
-Canonical dvdC_zmodPred x := ZmodPred (dvdC_zmod x).
- -
-Lemma dvdC_nat (p n : nat) : (p %| n)%C = (p %| n)%N.
- -
-Lemma dvdC_int (p : nat) x : x \in Cint → (p %| x)%C = (p %| `|floorC x |)%N.
- -
-

- -

- Elementary modular arithmetic. -

- -
-Lemma eqCmod_refl e x : (x == x %[mod e ])%C.
- -
-Lemma eqCmodm0 e : (e == 0 %[mod e ])%C.
-Hint Resolve eqCmod_refl eqCmodm0 : core.
- -
-Lemma eqCmod0 e x : (x == 0 %[mod e ])%C = (e %| x)%C.
- -
-Lemma eqCmod_sym e x y : ((x == y %[mod e ]) = (y == x %[mod e ]))%C.
- -
-Lemma eqCmod_trans e y x z :
-  (x == y %[mod e ] → y == z %[mod e ] → x == z %[mod e ])%C.
- -
-Lemma eqCmod_transl e x y z :
-  (x == y %[mod e ])%C → (x == z %[mod e ])%C = (y == z %[mod e ])%C.
- -
-Lemma eqCmod_transr e x y z :
-  (x == y %[mod e ])%C → (z == x %[mod e ])%C = (z == y %[mod e ])%C.
- -
-Lemma eqCmodN e x y : (- x == y %[mod e ])%C = (x == - y %[mod e ])%C.
- -
-Lemma eqCmodDr e x y z : (y + x == z + x %[mod e ])%C = (y == z %[mod e ])%C.
- -
-Lemma eqCmodDl e x y z : (x + y == x + z %[mod e ])%C = (y == z %[mod e ])%C.
- -
-Lemma eqCmodD e x1 x2 y1 y2 :
-  (x1 == x2 %[mod e ] → y1 == y2 %[mod e ] → x1 + y1 == x2 + y2 %[mod e ])%C.
- -
-Lemma eqCmod_nat (e m n : nat) : (m == n %[mod e ])%C = (m == n %[mod e ]).
- -
-Lemma eqCmod0_nat (e m : nat) : (m == 0 %[mod e ])%C = (e %| m)%N.
- -
-Lemma eqCmodMr e :
-  {in Cint , ∀ z x y, x == y %[mod e ] → x × z == y × z %[mod e ]}%C.
- -
-Lemma eqCmodMl e :
-  {in Cint , ∀ z x y, x == y %[mod e ] → z × x == z × y %[mod e ]}%C.
- -
-Lemma eqCmodMl0 e : {in Cint , ∀ x, x × e == 0 %[mod e ]}%C.
- -
-Lemma eqCmodMr0 e : {in Cint , ∀ x, e × x == 0 %[mod e ]}%C.
- -
-Lemma eqCmod_addl_mul e : {in Cint , ∀ x y, x × e + y == y %[mod e ]}%C.
- -
-Lemma eqCmodM e : {in Cint & Cint , ∀ x1 y2 x2 y1,
-  x1 == x2 %[mod e ] → y1 == y2 %[mod e ] → x1 × y1 == x2 × y2 %[mod e ]}%C.
- -
-

- -

- Rational number subset. -

- -
-Lemma ratCK : cancel QtoC CtoQ.
- -
-Lemma getCratK : {in Crat , cancel CtoQ QtoC }.
- -
-Lemma Crat_rat (a : rat) : QtoC a \in Crat.
- -
-Lemma CratP x : reflect (∃ a, x = QtoC a) (x \in Crat).
- -
-Lemma Crat0 : 0 \in Crat.
-Lemma Crat1 : 1 \in Crat.
-Hint Resolve Crat0 Crat1 : core.
- -
-Fact Crat_key : pred_key Crat.
-Fact Crat_divring_closed : divring_closed Crat.
-Canonical Crat_keyed := KeyedPred Crat_key.
-Canonical Crat_opprPred := OpprPred Crat_divring_closed.
-Canonical Crat_addrPred := AddrPred Crat_divring_closed.
-Canonical Crat_mulrPred := MulrPred Crat_divring_closed.
-Canonical Crat_zmodPred := ZmodPred Crat_divring_closed.
-Canonical Crat_semiringPred := SemiringPred Crat_divring_closed.
-Canonical Crat_smulrPred := SmulrPred Crat_divring_closed.
-Canonical Crat_divrPred := DivrPred Crat_divring_closed.
-Canonical Crat_subringPred := SubringPred Crat_divring_closed.
-Canonical Crat_sdivrPred := SdivrPred Crat_divring_closed.
-Canonical Crat_divringPred := DivringPred Crat_divring_closed.
- -
-Lemma rpred_Crat
-        (S : {pred algC }) (ringS : divringPred S) (kS : keyed_pred ringS) :
-  {subset Crat ≤ kS }.
- -
-Lemma conj_Crat z : z \in Crat → z ^* = z.
- -
-Lemma Creal_Crat : {subset Crat ≤ Creal }.
- -
-Lemma Cint_rat a : (QtoC a \in Cint ) = (a \in Qint ).
- -
-Lemma minCpolyP x :
-   {p | minCpoly x = pQtoC p ∧ p \is monic
-      & ∀ q, root (pQtoC q) x = (p %| q)%R}.
- -
-Lemma minCpoly_monic x : minCpoly x \is monic.
- -
-Lemma minCpoly_eq0 x : (minCpoly x == 0) = false.
- -
-Lemma root_minCpoly x : root (minCpoly x) x.
- -
-Lemma size_minCpoly x : (1 < size (minCpoly x))%N.
- -
-

- -

- Basic properties of automorphisms. -

-Section AutC.
- -
-Implicit Type nu : {rmorphism algC → algC }.
- -
-Lemma aut_Cnat nu : {in Cnat , nu =1 id }.
- -
-Lemma aut_Cint nu : {in Cint , nu =1 id }.
- -
-Lemma aut_Crat nu : {in Crat , nu =1 id }.
- -
-Lemma Cnat_aut nu x : (nu x \in Cnat ) = (x \in Cnat ).
- -
-Lemma Cint_aut nu x : (nu x \in Cint ) = (x \in Cint ).
- -
-Lemma Crat_aut nu x : (nu x \in Crat ) = (x \in Crat ).
- -
-Lemma algC_invaut_subproof nu x : {y | nu y = x }.
-Definition algC_invaut nu x := sval (algC_invaut_subproof nu x).
- -
-Lemma algC_invautK nu : cancel (algC_invaut nu) nu.
- -
-Lemma algC_autK nu : cancel nu (algC_invaut nu).
- -
-Fact algC_invaut_is_rmorphism nu : rmorphism (algC_invaut nu).
- Canonical algC_invaut_additive nu := Additive (algC_invaut_is_rmorphism nu).
-Canonical algC_invaut_rmorphism nu := RMorphism (algC_invaut_is_rmorphism nu).
- -
-Lemma minCpoly_aut nu x : minCpoly (nu x) = minCpoly x.
- -
-End AutC.
- -
-Section AutLmodC.
- -
-Variables (U V : lmodType algC) (f : {additive U → V }).
- -
-Lemma raddfZ_Cnat a u : a \in Cnat → f (a *: u) = a *: f u.
- -
-Lemma raddfZ_Cint a u : a \in Cint → f (a *: u) = a *: f u.
- -
-End AutLmodC.
- -
-Section PredCmod.
- -
-Variable V : lmodType algC.
- -
-Lemma rpredZ_Cnat S (addS : @addrPred V S) (kS : keyed_pred addS) :
- {in Cnat & kS , ∀ z u, z *: u \in kS }.
- -
-Lemma rpredZ_Cint S (subS : @zmodPred V S) (kS : keyed_pred subS) :
- {in Cint & kS , ∀ z u, z *: u \in kS }.
- -
-End PredCmod.
- -
-End AlgebraicsTheory.
-Hint Resolve Creal0 Creal1 Cnat_nat Cnat0 Cnat1 Cint0 Cint1 floorC0 Crat0 Crat1 : core.
-Hint Resolve dvdC0 dvdC_refl eqCmod_refl eqCmodm0 : core.
-