Library mathcomp.field.algC
+ +
+(* (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 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.
+ +
+
+
++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.closed_fields_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}.
+ +
+CoInductive 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_class := fun x : algC ⇒ ratr (getCrat x) == x.
+ +
+Definition floorC x := sval (floorC_subproof x).
+Definition Cint : pred_class := fun x : algC ⇒ (floorC x)%:~R == x.
+ +
+Definition truncC x := if x ≥ 0 then `|floorC x|%N else 0%N.
+Definition Cnat : pred_class := fun x : algC ⇒ (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_class :=
+ fun y : algC ⇒ 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).
+ +
+
+
++ 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.closed_fields_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}.
+ +
+CoInductive 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_class := fun x : algC ⇒ ratr (getCrat x) == x.
+ +
+Definition floorC x := sval (floorC_subproof x).
+Definition Cint : pred_class := fun x : algC ⇒ (floorC x)%:~R == x.
+ +
+Definition truncC x := if x ≥ 0 then `|floorC x|%N else 0%N.
+Definition Cnat : pred_class := fun x : algC ⇒ (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_class :=
+ fun y : algC ⇒ 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).
+ +
+
+ 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 _.
+ +
+
+
++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.
+ +
+
+
++ 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.
+
+
+
+
+ Real number subset.
+
+
+
+
+Lemma Creal0 : 0 \is Creal.
+Lemma Creal1 : 1 \is Creal.
+Hint Resolve Creal0 Creal1. (* Trivial cannot resolve a general real0 hint. *)
+ +
+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.
+ +
+
+
++Lemma Creal0 : 0 \is Creal.
+Lemma Creal1 : 1 \is Creal.
+Hint Resolve Creal0 Creal1. (* Trivial cannot resolve a general real0 hint. *)
+ +
+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.
+ +
+
+ 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.
+ +
+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 (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.
+ +
+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|.
+ +
+
+
++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.
+ +
+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 (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.
+ +
+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 (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.
+ +
+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.
+ +
+
+
++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 (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.
+ +
+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.
+ +
+
+
++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.
+ +
+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.
+ +
+
+
++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.
+ +
+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.
+ +
+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.
+ +
+
+
++Lemma eqCmod_refl e x : (x == x %[mod e])%C.
+ +
+Lemma eqCmodm0 e : (e == 0 %[mod e])%C.
+Hint Resolve eqCmod_refl eqCmodm0.
+ +
+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.
+ +
+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 (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.
+ +
+
+
++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.
+ +
+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 (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.
+Hint Resolve dvdC0 dvdC_refl eqCmod_refl eqCmodm0.
+
++ +
+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.
+Hint Resolve dvdC0 dvdC_refl eqCmod_refl eqCmodm0.
+