Library mathcomp.field.algC

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
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. 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). 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). In addition, we provide: 'i == the imaginary number (:= sqrtC (-1)). 'Re z == the real component of z. 'Im z == the imaginary component of z. 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 conj : {rmorphism type → type }.
Axiom conjK : involutive conj.
Axiom normK : ∀ x, `|x | ^+ 2 = x × conj x.

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).

End Implementation.

Definition divisor := Implementation.type.

Module Internals.

Import Implementation.

Fact algCi_subproof : {i : algC | i ^+ 2 = -1}.

Let Re2 z := z + z ^*.
Definition nnegIm z := 0 ≤ sval algCi_subproof × (z ^* - z ).
Definition argCle y z := nnegIm z ==> nnegIm y && (Re2 z ≤ Re2 y ).

CoInductive rootC_spec n (x : algC) : Type :=
  RootCspec (y : algC) of if (n > 0)%N then y ^+ n = x else y = 0
                        & ∀ z, (n > 0)%N → z ^+ n = x → argCle y z.

Fact rootC_subproof n x : rootC_spec n x.

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.
Notation conjC := conj.
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.
Notation "x ^*" := (conjC x) (at level 2, format "x ^*") : C_core_scope.
Notation "x ^*" := x^* (only parsing) : C_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.

Notation algCeq := eqType.
Notation algCzmod := zmodType.
Notation algCring := ringType.
Notation algCuring := unitRingType.
Notation algCnum := numDomainType.
Notation algCfield := fieldType.
Notation algCnumField := numFieldType.

Definition rootC n x := let: RootCspec y _ _ := rootC_subproof n x in y.
Notation "n .-root" := (rootC n) (at level 2, format "n .-root") : C_core_scope.
Notation "n .-root" := (rootC n) (only parsing) : C_scope.
Notation sqrtC := 2.-root.

Definition algCi := sqrtC (-1).
Notation "'i" := algCi (at level 0) : C_core_scope.
Notation "'i" := 'i (only parsing) : C_scope.

Definition algRe x := (x + x ^*) / 2%:R.
Definition algIm x := 'i × (x ^* - x ) / 2%:R.
Notation "'Re z" := (algRe z) (at level 10, z at level 8) : C_core_scope.
Notation "'Im z" := (algIm z) (at level 10, z at level 8) : C_core_scope.
Notation "'Re z" := ('Re z) (only parsing) : C_scope.
Notation "'Im z" := ('Im z) (only parsing) : C_scope.

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 _.

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 conjCK : involutive conjC := Algebraics.Implementation.conjK.
Definition normCK x : `|x | ^+ 2 = x × x ^* := Algebraics.Implementation.normK x.
Definition algC_algebraic x := Algebraics.Implementation.algebraic x.

Lemma normCKC x : `|x | ^+ 2 = x ^* × x.

Lemma mul_conjC_ge0 x : 0 ≤ x × x ^*.

Lemma mul_conjC_gt0 x : (0 < x × x ^*) = (x != 0).

Lemma mul_conjC_eq0 x : (x × x ^* == 0) = (x == 0).

Lemma conjC_ge0 x : (0 ≤ x ^*) = (0 ≤ x ).

Lemma conjC_nat n : (n %:R )^* = n %:R.
Lemma conjC0 : 0^* = 0.
Lemma conjC1 : 1^* = 1.
Lemma conjC_eq0 x : (x ^* == 0) = (x == 0).

Lemma invC_norm x : x ^-1 = `|x | ^- 2 × x ^*.

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 CrealE x : (x \is Creal ) = (x ^* == x ).

Lemma CrealP {x} : reflect (x ^* = x) (x \is Creal).

Lemma conj_Creal x : x \is Creal → x ^* = x.

Lemma conj_normC z : `|z |^* = `|z |.

Lemma geC0_conj x : 0 ≤ x → x ^* = x.

Lemma geC0_unit_exp x n : 0 ≤ x → (x ^+ n .+1 == 1) = (x == 1).

Elementary properties of roots.

Ltac case_rootC := rewrite /rootC; case: (rootC_subproof _ _).

Lemma root0C x : 0.-root x = 0.

Lemma rootCK n : (n > 0)%N → cancel n .-root (fun x ⇒ x ^+ n).

Lemma root1C x : 1.-root x = x.

Lemma rootC0 n : n .-root 0 = 0.

Lemma rootC_inj n : (n > 0)%N → injective n .-root.

Lemma eqr_rootC n : (n > 0)%N → {mono n .-root : x y / x == y}.

Lemma rootC_eq0 n x : (n > 0)%N → (n .-root x == 0) = (x == 0).

Rectangular coordinates.

Lemma sqrCi : 'i ^+ 2 = -1.

Lemma nonRealCi : 'i \isn't Creal.

Lemma neq0Ci : 'i != 0.

Lemma normCi : `|'i | = 1.

Lemma invCi : 'i ^-1 = - 'i.

Lemma conjCi : 'i ^* = - 'i.

Lemma algCrect x : x = 'Re x + 'i × 'Im x.

Lemma Creal_Re x : 'Re x \is Creal.

Lemma Creal_Im x : 'Im x \is Creal.
Hint Resolve Creal_Re Creal_Im.

Fact algRe_is_additive : additive algRe.
Canonical algRe_additive := Additive algRe_is_additive.

Fact algIm_is_additive : additive algIm.
Canonical algIm_additive := Additive algIm_is_additive.

Lemma Creal_ImP z : reflect ('Im z = 0) (z \is Creal).

Lemma Creal_ReP z : reflect ('Re z = z) (z \in Creal).

Lemma algReMl : {in Creal , ∀ x, {morph algRe : z / x × z}}.

Lemma algReMr : {in Creal , ∀ x, {morph algRe : z / z × x }}.

Lemma algImMl : {in Creal , ∀ x, {morph algIm : z / x × z}}.

Lemma algImMr : {in Creal , ∀ x, {morph algIm : z / z × x }}.

Lemma algRe_i : 'Re 'i = 0.

Lemma algIm_i : 'Im 'i = 1.

Lemma algRe_conj z : 'Re z ^* = 'Re z.

Lemma algIm_conj z : 'Im z ^* = - 'Im z.

Lemma algRe_rect : {in Creal &, ∀ x y, 'Re (x + 'i × y ) = x }.

Lemma algIm_rect : {in Creal &, ∀ x y, 'Im (x + 'i × y ) = y }.

Lemma conjC_rect : {in Creal &, ∀ x y, (x + 'i × y )^* = x - 'i × y }.

Lemma addC_rect x1 y1 x2 y2 :
  (x1 + 'i × y1 ) + (x2 + 'i × y2 ) = x1 + x2 + 'i × (y1 + y2 ).

Lemma oppC_rect x y : - (x + 'i × y ) = - x + 'i × (- y ).

Lemma subC_rect x1 y1 x2 y2 :
  (x1 + 'i × y1 ) - (x2 + 'i × y2 ) = x1 - x2 + 'i × (y1 - y2 ).

Lemma mulC_rect x1 y1 x2 y2 :
  (x1 + 'i × y1 ) × (x2 + 'i × y2 )
      = x1 × x2 - y1 × y2 + 'i × (x1 × y2 + x2 × y1 ).

Lemma normC2_rect :
  {in Creal &, ∀ x y, `|x + 'i × y | ^+ 2 = x ^+ 2 + y ^+ 2}.

Lemma normC2_Re_Im z : `|z | ^+ 2 = 'Re z ^+ 2 + 'Im z ^+ 2.

Lemma invC_rect :
  {in Creal &, ∀ x y, (x + 'i × y )^-1 = (x - 'i × y ) / (x ^+ 2 + y ^+ 2)}.

Lemma lerif_normC_Re_Creal z : `|'Re z | ≤ `|z | ?= iff (z \is Creal ).

Lemma lerif_Re_Creal z : 'Re z ≤ `|z | ?= iff (0 ≤ z ).

Equality from polar coordinates, for the upper plane.

Lemma eqC_semipolar x y :
`|x | = `|y | → 'Re x = 'Re y → 0 ≤ 'Im x × 'Im y → x = y.

Nth roots.

Let argCleP y z :
reflect (0 ≤ 'Im z → 0 ≤ 'Im y ∧ 'Re z ≤ 'Re y) (argCle y z).

Lemma rootC_Re_max n x y :
(n > 0)%N → y ^+ n = x → 0 ≤ 'Im y → 'Re y ≤ 'Re (n .-root%C x ).

Let neg_unity_root n : (n > 1)%N → exists2 w : algC , w ^+ n = 1 & 'Re w < 0.

Lemma Im_rootC_ge0 n x : (n > 1)%N → 0 ≤ 'Im (n .-root x ).

Lemma rootC_lt0 n x : (1 < n)%N → (n .-root x < 0) = false.

Lemma rootC_ge0 n x : (n > 0)%N → (0 ≤ n .-root x ) = (0 ≤ x ).

Lemma rootC_gt0 n x : (n > 0)%N → (n .-root x > 0) = (x > 0).

Lemma rootC_le0 n x : (1 < n)%N → (n .-root x ≤ 0) = (x == 0).

Lemma ler_rootCl n : (n > 0)%N → {in Num.nneg , {mono n .-root : x y / x ≤ y}}.

Lemma ler_rootC n : (n > 0)%N → {in Num.nneg &, {mono n .-root : x y / x ≤ y}}.

Lemma ltr_rootCl n : (n > 0)%N → {in Num.nneg , {mono n .-root : x y / x < y}}.

Lemma ltr_rootC n : (n > 0)%N → {in Num.nneg &, {mono n .-root : x y / x < y}}.

Lemma exprCK n x : (0 < n)%N → 0 ≤ x → n .-root (x ^+ n) = x.

Lemma norm_rootC n x : `|n .-root x | = n .-root `|x |.

Lemma rootCX n x k : (n > 0)%N → 0 ≤ x → n .-root (x ^+ k) = n .-root x ^+ k.

Lemma rootC1 n : (n > 0)%N → n .-root 1 = 1.

Lemma rootCpX n x k : (k > 0)%N → 0 ≤ x → n .-root (x ^+ k) = n .-root x ^+ k.

Lemma rootCV n x : (n > 0)%N → 0 ≤ x → n .-root x ^-1 = (n .-root x )^-1.

Lemma rootC_eq1 n x : (n > 0)%N → (n .-root x == 1) = (x == 1).

Lemma rootC_ge1 n x : (n > 0)%N → (n .-root x ≥ 1) = (x ≥ 1).

Lemma rootC_gt1 n x : (n > 0)%N → (n .-root x > 1) = (x > 1).

Lemma rootC_le1 n x : (n > 0)%N → 0 ≤ x → (n .-root x ≤ 1) = (x ≤ 1).

Lemma rootC_lt1 n x : (n > 0)%N → 0 ≤ x → (n .-root x < 1) = (x < 1).

Lemma rootCMl n x z : 0 ≤ x → n .-root (x × z) = n .-root x × n .-root z.

Lemma rootCMr n x z : 0 ≤ x → n .-root (z × x) = n .-root z × n .-root x.

More properties of n.-root will be established in cyclotomic.v.

The proper form of the Arithmetic - Geometric Mean inequality.

Lemma lerif_rootC_AGM (I : finType) (A : pred I) (n := #|A |) E :
    {in A , ∀ i, 0 ≤ E i } →
  n .-root (\prod_(i in A ) E i) ≤ (\sum_(i in A ) E i) / n %:R
                             ?= iff [∀ i in A , ∀ j in A , E i == E j].

Square root.

Lemma sqrtC0 : sqrtC 0 = 0.
Lemma sqrtC1 : sqrtC 1 = 1.
Lemma sqrtCK x : sqrtC x ^+ 2 = x.
Lemma sqrCK x : 0 ≤ x → sqrtC (x ^+ 2) = x.

Lemma sqrtC_ge0 x : (0 ≤ sqrtC x ) = (0 ≤ x ).
Lemma sqrtC_eq0 x : (sqrtC x == 0) = (x == 0).
Lemma sqrtC_gt0 x : (sqrtC x > 0) = (x > 0).
Lemma sqrtC_lt0 x : (sqrtC x < 0) = false.
Lemma sqrtC_le0 x : (sqrtC x ≤ 0) = (x == 0).

Lemma ler_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x ≤ y}}.
Lemma ltr_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x < y}}.
Lemma eqr_sqrtC : {mono sqrtC : x y / x == y}.
Lemma sqrtC_inj : injective sqrtC.
Lemma sqrtCM : {in Num.nneg &, {morph sqrtC : x y / x × y}}.

Lemma sqrCK_P x : reflect (sqrtC (x ^+ 2) = x) ((0 ≤ 'Im x ) && ~~ (x < 0)).

Lemma normC_def x : `|x | = sqrtC (x × x ^*).

Lemma norm_conjC x : `|x ^*| = `|x |.

Lemma normC_rect :
{in Creal &, ∀ x y, `|x + 'i × y | = sqrtC (x ^+ 2 + y ^+ 2)}.

Lemma normC_Re_Im z : `|z | = sqrtC ('Re z ^+ 2 + 'Im z ^+ 2).

Norm sum (in)equalities.

Lemma normC_add_eq x y :
    `|x + y | = `|x | + `|y | →
  {t : algC | `|t| == 1 & (x , y ) = (`|x | × t, `|y | × t)}.

Lemma normC_sum_eq (I : finType) (P : pred I) (F : I → algC) :
     `|\sum_(i | P i) F i| = \sum_(i | P i) `|F i| →
   {t : algC | `|t| == 1 & ∀ i, P i → F i = `|F i | × t}.

Lemma normC_sum_eq1 (I : finType) (P : pred I) (F : I → algC) :
    `|\sum_(i | P i) F i| = (\sum_(i | P i) `|F i|) →
     (∀ i, P i → `|F i | = 1) →
   {t : algC | `|t| == 1 & ∀ i, P i → F i = t}.

Lemma normC_sum_upper (I : finType) (P : pred I) (F G : I → algC) :
     (∀ i, P i → `|F i | ≤ G i ) →
     \sum_(i | P i) F i = \sum_(i | P i) G i →
   ∀ i, P i → F i = G i.

Lemma normC_sub_eq x y :
  `|x - y | = `|x | - `|y | → {t | `|t| == 1 & (x , y ) = (`|x | × t, `|y | × t)}.

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 |.

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.

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.

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.

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.

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.