Library mathcomp.field.algC
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice.
From mathcomp Require Import div fintype path bigop finset prime order ssralg.
From mathcomp Require Import poly polydiv mxpoly generic_quotient countalg.
From mathcomp Require Import ssrnum closed_field ssrint archimedean rat intdiv.
From mathcomp Require Import algebraics_fundamentals.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice.
From mathcomp Require Import div fintype path bigop finset prime order ssralg.
From mathcomp Require Import poly polydiv mxpoly generic_quotient countalg.
From mathcomp Require Import ssrnum closed_field ssrint archimedean rat intdiv.
From mathcomp Require Import algebraics_fundamentals.
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.
getCrat z == some a : rat such that ratr a = z, provided z \in Crat.
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.
Declare Scope C_scope.
Declare Scope C_core_scope.
Declare Scope C_expanded_scope.
Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Lemma nz2: 2 != 0 :> L.
Lemma mul2I: injective (fun z : L ⇒ z *+ 2).
Definition sqrt x : L :=
sval (sig_eqW (@solve_monicpoly _ 2%N (nth 0 [:: x]) isT)).
Lemma sqrtK x: sqrt x ^+ 2 = x.
Lemma sqrtE x y: y ^+ 2 = x → {b : bool | y = (-1) ^+ b × sqrt x}.
Definition i := sqrt (- 1).
Lemma sqrMi x: (i × x) ^+ 2 = - x ^+ 2.
Lemma iJ : conj i = - i.
Definition norm x := sqrt x × conj (sqrt x).
Lemma normK x : norm x ^+ 2 = x × conj x.
Lemma normE x y : y ^+ 2 = x → norm x = y × conj y.
Lemma norm_eq0 x : norm x = 0 → x = 0.
Lemma normM x y : norm (x × y) = norm x × norm y.
Lemma normN x : norm (- x) = norm x.
Definition le x y := norm (y - x) == y - x.
Definition lt x y := (y != x) && le x y.
Lemma posE x: le 0 x = (norm x == x).
Lemma leB x y: le x y = le 0 (y - x).
Lemma posP x : reflect (∃ y, x = y × conj y) (le 0 x).
Lemma posJ x : le 0 x → conj x = x.
Lemma pos_linear x y : le 0 x → le 0 y → le x y || le y x.
Lemma sposDl x y : lt 0 x → le 0 y → lt 0 (x + y).
Lemma sposD x y : lt 0 x → lt 0 y → lt 0 (x + y).
Lemma normD x y : le (norm (x + y)) (norm x + norm y).
Module Algebraics.
Module Type Specification.
Parameter type : Type.
Parameter conjMixin : Num.ClosedField type.
Parameter isCountable : Countable type.
Note that this cannot be included in conjMixin since a few proofs
depend from nat_num being definitionally equal to (trunc x)%:R == x
Axiom archimedean : Num.archimedean_axiom (Num.ClosedField.Pack conjMixin).
Axiom algebraic : integralRange (@ratr (Num.ClosedField.Pack conjMixin)).
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 L' : Type := eta L.
Notation cfType := (L' : closedFieldType).
Definition QtoL : {rmorphism _ → _} := @ratr cfType.
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 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.
Fact CtoL_is_additive : additive CtoL.
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.
Fact CtoL_is_multiplicative : multiplicative CtoL.
Fact mulVf u : u != 0 → inv u × u = 1.
Fact inv0 : inv 0 = 0.
Fact closedFieldAxiom : GRing.closed_field_axiom type.
Fact conj_subproof u : integralOver QtoL (conjL (CtoL u)).
Fact conj_is_semi_additive : semi_additive (fun u ⇒ LtoC (conj_subproof u)).
Fact conj_is_additive : {morph (fun u ⇒ LtoC (conj_subproof u)) : x / - x}.
Fact conj_is_multiplicative : multiplicative (fun u ⇒ LtoC (conj_subproof u)).
Definition conj : {rmorphism type → type} :=
GRing.RMorphism.Pack
(GRing.RMorphism.Class
(GRing.isSemiAdditive.Build _ _ _ conj_is_semi_additive)
(GRing.isMultiplicative.Build _ _ _ conj_is_multiplicative)).
Lemma conjK : involutive conj.
Fact conj_nt : ¬ conj =1 id.
Definition conjMixin := Num.ClosedField.on type.
Lemma algebraic : integralRange (@ratr type).
Fact archimedean : Num.archimedean_axiom type.
Definition isCountable := Countable.on type.
End Implementation.
Definition divisor := Implementation.type.
#[export] HB.instance Definition _ := Implementation.conjMixin.
#[export] HB.instance Definition _ :=
Num.NumDomain_bounded_isArchimedean.Build Implementation.type
Implementation.archimedean.
#[export] HB.instance Definition _ := Implementation.isCountable.
Module Internals.
Import Implementation.
Local Notation algC := type.
Local Notation QtoC := (ratr : rat → algC).
Local Notation pQtoC := (map_poly QtoC).
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 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.
Notation algCeq := (type : eqType).
Notation algCzmod := (type : zmodType).
Notation algCring := (type : ringType).
Notation algCuring := (type : unitRingType).
Notation algCnum := (type : numDomainType).
Notation algCfield := (type : fieldType).
Notation algCnumField := (type : numFieldType).
Notation algCnumClosedField := (type : numClosedFieldType).
Notation Creal := (@Num.Def.Rreal algCnum).
Definition getCrat := let: GetCrat_spec CtoQ _ := getCrat_subproof in CtoQ.
Definition Crat : {pred algC} := fun x ⇒ ratr (getCrat x) == 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 Num.int.
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.
Module HBExports. End HBExports.
End Algebraics.
Export Algebraics.Exports.
Export Algebraics.HBExports.
Section AlgebraicsTheory.
Implicit Types (x y z : algC) (n : nat) (m : int) (b : bool).
Import Algebraics.Internals.
Local Notation ZtoQ := (intr : int → rat).
Local Notation ZtoC := (intr : int → algC).
Local Notation QtoC := (ratr : rat → algC).
Local Notation CtoQ := getCrat.
Local Notation intrp := (map_poly intr).
Local Notation pZtoQ := (map_poly ZtoQ).
Local Notation pZtoC := (map_poly ZtoC).
Local Notation pQtoC := (map_poly ratr).
Let intr_inj_ZtoC := (intr_inj : injective ZtoC).
#[local] Hint Resolve intr_inj_ZtoC : core.
Axiom algebraic : integralRange (@ratr (Num.ClosedField.Pack conjMixin)).
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 L' : Type := eta L.
Notation cfType := (L' : closedFieldType).
Definition QtoL : {rmorphism _ → _} := @ratr cfType.
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 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.
Fact CtoL_is_additive : additive CtoL.
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.
Fact CtoL_is_multiplicative : multiplicative CtoL.
Fact mulVf u : u != 0 → inv u × u = 1.
Fact inv0 : inv 0 = 0.
Fact closedFieldAxiom : GRing.closed_field_axiom type.
Fact conj_subproof u : integralOver QtoL (conjL (CtoL u)).
Fact conj_is_semi_additive : semi_additive (fun u ⇒ LtoC (conj_subproof u)).
Fact conj_is_additive : {morph (fun u ⇒ LtoC (conj_subproof u)) : x / - x}.
Fact conj_is_multiplicative : multiplicative (fun u ⇒ LtoC (conj_subproof u)).
Definition conj : {rmorphism type → type} :=
GRing.RMorphism.Pack
(GRing.RMorphism.Class
(GRing.isSemiAdditive.Build _ _ _ conj_is_semi_additive)
(GRing.isMultiplicative.Build _ _ _ conj_is_multiplicative)).
Lemma conjK : involutive conj.
Fact conj_nt : ¬ conj =1 id.
Definition conjMixin := Num.ClosedField.on type.
Lemma algebraic : integralRange (@ratr type).
Fact archimedean : Num.archimedean_axiom type.
Definition isCountable := Countable.on type.
End Implementation.
Definition divisor := Implementation.type.
#[export] HB.instance Definition _ := Implementation.conjMixin.
#[export] HB.instance Definition _ :=
Num.NumDomain_bounded_isArchimedean.Build Implementation.type
Implementation.archimedean.
#[export] HB.instance Definition _ := Implementation.isCountable.
Module Internals.
Import Implementation.
Local Notation algC := type.
Local Notation QtoC := (ratr : rat → algC).
Local Notation pQtoC := (map_poly QtoC).
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 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.
Notation algCeq := (type : eqType).
Notation algCzmod := (type : zmodType).
Notation algCring := (type : ringType).
Notation algCuring := (type : unitRingType).
Notation algCnum := (type : numDomainType).
Notation algCfield := (type : fieldType).
Notation algCnumField := (type : numFieldType).
Notation algCnumClosedField := (type : numClosedFieldType).
Notation Creal := (@Num.Def.Rreal algCnum).
Definition getCrat := let: GetCrat_spec CtoQ _ := getCrat_subproof in CtoQ.
Definition Crat : {pred algC} := fun x ⇒ ratr (getCrat x) == 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 Num.int.
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.
Module HBExports. End HBExports.
End Algebraics.
Export Algebraics.Exports.
Export Algebraics.HBExports.
Section AlgebraicsTheory.
Implicit Types (x y z : algC) (n : nat) (m : int) (b : bool).
Import Algebraics.Internals.
Local Notation ZtoQ := (intr : int → rat).
Local Notation ZtoC := (intr : int → algC).
Local Notation QtoC := (ratr : rat → algC).
Local Notation CtoQ := getCrat.
Local Notation intrp := (map_poly intr).
Local Notation pZtoQ := (map_poly ZtoQ).
Local Notation pZtoC := (map_poly ZtoC).
Local Notation pQtoC := (map_poly ratr).
Let intr_inj_ZtoC := (intr_inj : injective ZtoC).
#[local] Hint Resolve intr_inj_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^-1 + 7%:%^-1 < 2%:%^-1 :> algC.
Missing norm and integer exponent, due to gaps in ssrint and rat.
Definition CratrE :=
let CnF : numClosedFieldType := algC in
let QtoCm : {rmorphism _ → _} := @ratr CnF in
((rmorph0 QtoCm, rmorph1 QtoCm, rmorphMn QtoCm, rmorphN QtoCm, rmorphD QtoCm),
(rmorphM QtoCm, rmorphXn 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 : numClosedFieldType := algC in
let ZtoCm : {rmorphism _ → _} := *~%R (1 : CnF) in
((rmorph0 ZtoCm, rmorph1 ZtoCm, rmorphMn ZtoCm, rmorphN ZtoCm, rmorphD ZtoCm),
(rmorphM ZtoCm, rmorphXn ZtoCm),
(rmorphMz ZtoCm, @intr_norm CnF, @intr_sg CnF),
=^~ (@ler_int CnF, @ltr_int CnF, (inj_eq (@intr_inj CnF)))).
Let nz2 : 2 != 0 :> algC.
let CnF : numClosedFieldType := algC in
let QtoCm : {rmorphism _ → _} := @ratr CnF in
((rmorph0 QtoCm, rmorph1 QtoCm, rmorphMn QtoCm, rmorphN QtoCm, rmorphD QtoCm),
(rmorphM QtoCm, rmorphXn 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 : numClosedFieldType := algC in
let ZtoCm : {rmorphism _ → _} := *~%R (1 : CnF) in
((rmorph0 ZtoCm, rmorph1 ZtoCm, rmorphMn ZtoCm, rmorphN ZtoCm, rmorphD ZtoCm),
(rmorphM ZtoCm, rmorphXn ZtoCm),
(rmorphMz ZtoCm, @intr_norm CnF, @intr_sg CnF),
=^~ (@ler_int CnF, @ltr_int CnF, (inj_eq (@intr_inj CnF)))).
Let nz2 : 2 != 0 :> algC.
Conjugation and norm.
Real number subset.
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 divisibility.
Lemma dvdCP x y : reflect (exists2 z, z \in Num.int & 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 Num.int → (x %| z)%C → (x %| y × z)%C.
Lemma dvdC_mulr x y z : y \in Num.int → (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.
Lemma dvdC_zmod x : zmod_closed (dvdC x).
Lemma dvdC_nat (p n : nat) : (p %| n)%C = (p %| n)%N.
Lemma dvdC_int (p : nat) x :
x \in Num.int → (p %| x)%C = (p %| `|Num.floor 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 Num.int, ∀ z x y, x == y %[mod e] → x × z == y × z %[mod e]}%C.
Lemma eqCmodMl e :
{in Num.int, ∀ z x y, x == y %[mod e] → z × x == z × y %[mod e]}%C.
Lemma eqCmodMl0 e : {in Num.int, ∀ x, x × e == 0 %[mod e]}%C.
Lemma eqCmodMr0 e : {in Num.int, ∀ x, e × x == 0 %[mod e]}%C.
Lemma eqCmod_addl_mul e : {in Num.int, ∀ x y, x × e + y == y %[mod e]}%C.
Lemma eqCmodM e : {in Num.int & Num.int, ∀ 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.
#[local] Hint Resolve Crat0 Crat1 : core.
Fact Crat_divring_closed : divring_closed Crat.
Lemma rpred_Crat (S : divringClosed algC) : {subset Crat ≤ S}.
Lemma conj_Crat z : z \in Crat → z^* = z.
Lemma Creal_Crat : {subset Crat ≤ Creal}.
Lemma Cint_rat a : (QtoC a \in Num.int) = (a \in Num.int).
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_Crat nu : {in Crat, nu =1 id}.
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_additive nu : additive (algC_invaut nu).
Fact algC_invaut_is_rmorphism nu : multiplicative (algC_invaut nu).
Lemma minCpoly_aut nu x : minCpoly (nu x) = minCpoly x.
End AutC.
End AlgebraicsTheory.
#[global] Hint Resolve Crat0 Crat1 dvdC0 dvdC_refl eqCmod_refl eqCmodm0 : core.
Module mc_2_0.
Implicit Types (x y z : algC) (n : nat) (m : int) (b : bool).
Notation Cint := (Num.int : {pred algC}) (only parsing).
Notation Cnat := (Num.nat : {pred algC}) (only parsing).
Notation floorC := (Num.floor : algC → int) (only parsing).
Notation truncC := (Num.trunc : algC → nat) (only parsing).
Lemma Creal0 : 0 \is Creal.
Lemma Creal1 : 1 \is Creal.
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.
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 : subringClosed algC) x : x \in Cint → x \in S.
Lemma Cint0 : 0 \in Cint.
Lemma Cint1 : 1 \in Cint.
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 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) (~~ (1 ≤ x)).
Lemma truncC0 : truncC 0 = 0.
Lemma truncC1 : truncC 1 = 1.
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 : semiringClosed algC) x : x \in Cnat → x \in S.
Lemma Cnat_nat n : n%:R \in Cnat.
Lemma Cnat0 : 0 \in Cnat.
Lemma Cnat1 : 1 \in Cnat.
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 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.
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 Cnat_aut nu x : (nu x \in Cnat) = (x \in Cnat).
Lemma Cint_aut nu x : (nu x \in Cint) = (x \in Cint).
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 : addrClosed V) : {in Cnat & S, ∀ z u, z *: u \in S}.
Lemma rpredZ_Cint (S : zmodClosed V) : {in Cint & S, ∀ z u, z *: u \in S}.
End PredCmod.
End mc_2_0.
#[deprecated(since="mathcomp 2.1.0", note="Use Num.int instead.")]
Notation Cint := (Num.int : {pred algC}) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Num.nat instead.")]
Notation Cnat := (Num.nat : {pred algC}) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Num.floor instead.")]
Notation floorC := (Num.floor : algC → int) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Num.trunc instead.")]
Notation truncC := (Num.trunc : algC → nat) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use real0 instead.")]
Notation Creal0 := mc_2_0.Creal0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use real1 instead.")]
Notation Creal1 := mc_2_0.Creal1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floor_itv instead.")]
Notation floorC_itv := mc_2_0.floorC_itv (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floor_def instead.")]
Notation floorC_def := mc_2_0.floorC_def (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrKfloor instead.")]
Notation intCK := mc_2_0.intCK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorK instead.")]
Notation floorCK := mc_2_0.floorCK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floor0 instead.")]
Notation floorC0 := mc_2_0.floorC0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floor1 instead.")]
Notation floorC1 := mc_2_0.floorC1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorpK instead.")]
Notation floorCpK := mc_2_0.floorCpK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorpP instead.")]
Notation floorCpP := mc_2_0.floorCpP (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intr_int instead.")]
Notation Cint_int := mc_2_0.Cint_int (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrP instead.")]
Notation CintP := mc_2_0.CintP (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorD instead.")]
Notation floorCD := mc_2_0.floorCD (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorN instead.")]
Notation floorCN := mc_2_0.floorCN (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorM instead.")]
Notation floorCM := mc_2_0.floorCM (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorX instead.")]
Notation floorCX := mc_2_0.floorCX (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use rpred_int_num instead.")]
Notation rpred_Cint := mc_2_0.rpred_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use int_num0 instead.")]
Notation Cint0 := mc_2_0.Cint0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use int_num1 instead.")]
Notation Cint1 := mc_2_0.Cint1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Rreal_int instead.")]
Notation Creal_Cint := mc_2_0.Creal_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use conj_intr instead.")]
Notation conj_Cint := mc_2_0.conj_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intr_normK instead.")]
Notation Cint_normK := mc_2_0.Cint_normK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrEsign instead.")]
Notation CintEsign := mc_2_0.CintEsign (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc_itv instead.")]
Notation truncC_itv := mc_2_0.truncC_itv (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc_def instead.")]
Notation truncC_def := mc_2_0.truncC_def (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natRK instead.")]
Notation natCK := mc_2_0.natCK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natrP instead.")]
Notation CnatP := mc_2_0.CnatP (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use truncK instead.")]
Notation truncCK := mc_2_0.truncCK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc_gt0 instead.")]
Notation truncC_gt0 := mc_2_0.truncC_gt0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc0Pn instead.")]
Notation truncC0Pn := mc_2_0.truncC0Pn (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc0 instead.")]
Notation truncC0 := mc_2_0.truncC0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc1 instead.")]
Notation truncC1 := mc_2_0.truncC1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use truncD instead.")]
Notation truncCD := mc_2_0.truncCD (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use truncM instead.")]
Notation truncCM := mc_2_0.truncCM (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use truncX instead.")]
Notation truncCX := mc_2_0.truncCX (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use rpred_nat_num instead.")]
Notation rpred_Cnat := mc_2_0.rpred_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_nat instead.")]
Notation Cnat_nat := mc_2_0.Cnat_nat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use nat_num0 instead.")]
Notation Cnat0 := mc_2_0.Cnat0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use nat_num1 instead.")]
Notation Cnat1 := mc_2_0.Cnat1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_ge0 instead.")]
Notation Cnat_ge0 := mc_2_0.Cnat_ge0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_gt0 instead.")]
Notation Cnat_gt0 := mc_2_0.Cnat_gt0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use conj_natr instead.")]
Notation conj_Cnat := mc_2_0.conj_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use norm_natr instead.")]
Notation norm_Cnat := mc_2_0.norm_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Rreal_nat instead.")]
Notation Creal_Cnat := mc_2_0.Creal_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_sum_eq1 instead.")]
Notation Cnat_sum_eq1 := mc_2_0.Cnat_sum_eq1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_mul_eq1 instead.")]
Notation Cnat_mul_eq1 := mc_2_0.Cnat_mul_eq1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_prod_eq1 instead.")]
Notation Cnat_prod_eq1 := mc_2_0.Cnat_prod_eq1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intr_nat instead.")]
Notation Cint_Cnat := mc_2_0.Cint_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrE instead.")]
Notation CintE := mc_2_0.CintE (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_norm_int instead.")]
Notation Cnat_norm_Cint := mc_2_0.Cnat_norm_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natrEint instead.")]
Notation CnatEint := mc_2_0.CnatEint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrEge0 instead.")]
Notation CintEge0 := mc_2_0.CintEge0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_exp_even instead.")]
Notation Cnat_exp_even := mc_2_0.Cnat_exp_even (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use norm_intr_ge1 instead.")]
Notation norm_Cint_ge1 := mc_2_0.norm_Cint_ge1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use sqr_intr_ge1 instead.")]
Notation sqr_Cint_ge1 := mc_2_0.sqr_Cint_ge1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intr_ler_sqr instead.")]
Notation Cint_ler_sqr := mc_2_0.Cint_ler_sqr (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use aut_natr instead.")]
Notation aut_Cnat := mc_2_0.aut_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use aut_intr instead.")]
Notation aut_Cint := mc_2_0.aut_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_aut instead.")]
Notation Cnat_aut := mc_2_0.Cnat_aut (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intr_aut instead.")]
Notation Cint_aut := mc_2_0.Cint_aut (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use raddfZ_nat instead.")]
Notation raddfZ_Cnat := mc_2_0.raddfZ_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use raddfZ_int instead.")]
Notation raddfZ_Cint := mc_2_0.raddfZ_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use rpredZnat instead.")]
Notation rpredZ_Cnat := mc_2_0.rpredZ_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use rpredZint instead.")]
Notation rpredZ_Cint := mc_2_0.rpredZ_Cint (only parsing).
Implicit Type nu : {rmorphism algC → algC}.
Lemma aut_Crat nu : {in Crat, nu =1 id}.
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_additive nu : additive (algC_invaut nu).
Fact algC_invaut_is_rmorphism nu : multiplicative (algC_invaut nu).
Lemma minCpoly_aut nu x : minCpoly (nu x) = minCpoly x.
End AutC.
End AlgebraicsTheory.
#[global] Hint Resolve Crat0 Crat1 dvdC0 dvdC_refl eqCmod_refl eqCmodm0 : core.
Module mc_2_0.
Implicit Types (x y z : algC) (n : nat) (m : int) (b : bool).
Notation Cint := (Num.int : {pred algC}) (only parsing).
Notation Cnat := (Num.nat : {pred algC}) (only parsing).
Notation floorC := (Num.floor : algC → int) (only parsing).
Notation truncC := (Num.trunc : algC → nat) (only parsing).
Lemma Creal0 : 0 \is Creal.
Lemma Creal1 : 1 \is Creal.
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.
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 : subringClosed algC) x : x \in Cint → x \in S.
Lemma Cint0 : 0 \in Cint.
Lemma Cint1 : 1 \in Cint.
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 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) (~~ (1 ≤ x)).
Lemma truncC0 : truncC 0 = 0.
Lemma truncC1 : truncC 1 = 1.
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 : semiringClosed algC) x : x \in Cnat → x \in S.
Lemma Cnat_nat n : n%:R \in Cnat.
Lemma Cnat0 : 0 \in Cnat.
Lemma Cnat1 : 1 \in Cnat.
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 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.
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 Cnat_aut nu x : (nu x \in Cnat) = (x \in Cnat).
Lemma Cint_aut nu x : (nu x \in Cint) = (x \in Cint).
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 : addrClosed V) : {in Cnat & S, ∀ z u, z *: u \in S}.
Lemma rpredZ_Cint (S : zmodClosed V) : {in Cint & S, ∀ z u, z *: u \in S}.
End PredCmod.
End mc_2_0.
#[deprecated(since="mathcomp 2.1.0", note="Use Num.int instead.")]
Notation Cint := (Num.int : {pred algC}) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Num.nat instead.")]
Notation Cnat := (Num.nat : {pred algC}) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Num.floor instead.")]
Notation floorC := (Num.floor : algC → int) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Num.trunc instead.")]
Notation truncC := (Num.trunc : algC → nat) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use real0 instead.")]
Notation Creal0 := mc_2_0.Creal0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use real1 instead.")]
Notation Creal1 := mc_2_0.Creal1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floor_itv instead.")]
Notation floorC_itv := mc_2_0.floorC_itv (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floor_def instead.")]
Notation floorC_def := mc_2_0.floorC_def (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrKfloor instead.")]
Notation intCK := mc_2_0.intCK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorK instead.")]
Notation floorCK := mc_2_0.floorCK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floor0 instead.")]
Notation floorC0 := mc_2_0.floorC0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floor1 instead.")]
Notation floorC1 := mc_2_0.floorC1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorpK instead.")]
Notation floorCpK := mc_2_0.floorCpK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorpP instead.")]
Notation floorCpP := mc_2_0.floorCpP (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intr_int instead.")]
Notation Cint_int := mc_2_0.Cint_int (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrP instead.")]
Notation CintP := mc_2_0.CintP (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorD instead.")]
Notation floorCD := mc_2_0.floorCD (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorN instead.")]
Notation floorCN := mc_2_0.floorCN (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorM instead.")]
Notation floorCM := mc_2_0.floorCM (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use floorX instead.")]
Notation floorCX := mc_2_0.floorCX (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use rpred_int_num instead.")]
Notation rpred_Cint := mc_2_0.rpred_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use int_num0 instead.")]
Notation Cint0 := mc_2_0.Cint0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use int_num1 instead.")]
Notation Cint1 := mc_2_0.Cint1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Rreal_int instead.")]
Notation Creal_Cint := mc_2_0.Creal_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use conj_intr instead.")]
Notation conj_Cint := mc_2_0.conj_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intr_normK instead.")]
Notation Cint_normK := mc_2_0.Cint_normK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrEsign instead.")]
Notation CintEsign := mc_2_0.CintEsign (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc_itv instead.")]
Notation truncC_itv := mc_2_0.truncC_itv (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc_def instead.")]
Notation truncC_def := mc_2_0.truncC_def (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natRK instead.")]
Notation natCK := mc_2_0.natCK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natrP instead.")]
Notation CnatP := mc_2_0.CnatP (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use truncK instead.")]
Notation truncCK := mc_2_0.truncCK (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc_gt0 instead.")]
Notation truncC_gt0 := mc_2_0.truncC_gt0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc0Pn instead.")]
Notation truncC0Pn := mc_2_0.truncC0Pn (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc0 instead.")]
Notation truncC0 := mc_2_0.truncC0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use trunc1 instead.")]
Notation truncC1 := mc_2_0.truncC1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use truncD instead.")]
Notation truncCD := mc_2_0.truncCD (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use truncM instead.")]
Notation truncCM := mc_2_0.truncCM (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use truncX instead.")]
Notation truncCX := mc_2_0.truncCX (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use rpred_nat_num instead.")]
Notation rpred_Cnat := mc_2_0.rpred_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_nat instead.")]
Notation Cnat_nat := mc_2_0.Cnat_nat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use nat_num0 instead.")]
Notation Cnat0 := mc_2_0.Cnat0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use nat_num1 instead.")]
Notation Cnat1 := mc_2_0.Cnat1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_ge0 instead.")]
Notation Cnat_ge0 := mc_2_0.Cnat_ge0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_gt0 instead.")]
Notation Cnat_gt0 := mc_2_0.Cnat_gt0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use conj_natr instead.")]
Notation conj_Cnat := mc_2_0.conj_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use norm_natr instead.")]
Notation norm_Cnat := mc_2_0.norm_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Rreal_nat instead.")]
Notation Creal_Cnat := mc_2_0.Creal_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_sum_eq1 instead.")]
Notation Cnat_sum_eq1 := mc_2_0.Cnat_sum_eq1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_mul_eq1 instead.")]
Notation Cnat_mul_eq1 := mc_2_0.Cnat_mul_eq1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_prod_eq1 instead.")]
Notation Cnat_prod_eq1 := mc_2_0.Cnat_prod_eq1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intr_nat instead.")]
Notation Cint_Cnat := mc_2_0.Cint_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrE instead.")]
Notation CintE := mc_2_0.CintE (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_norm_int instead.")]
Notation Cnat_norm_Cint := mc_2_0.Cnat_norm_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natrEint instead.")]
Notation CnatEint := mc_2_0.CnatEint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrEge0 instead.")]
Notation CintEge0 := mc_2_0.CintEge0 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_exp_even instead.")]
Notation Cnat_exp_even := mc_2_0.Cnat_exp_even (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use norm_intr_ge1 instead.")]
Notation norm_Cint_ge1 := mc_2_0.norm_Cint_ge1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use sqr_intr_ge1 instead.")]
Notation sqr_Cint_ge1 := mc_2_0.sqr_Cint_ge1 (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intr_ler_sqr instead.")]
Notation Cint_ler_sqr := mc_2_0.Cint_ler_sqr (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use aut_natr instead.")]
Notation aut_Cnat := mc_2_0.aut_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use aut_intr instead.")]
Notation aut_Cint := mc_2_0.aut_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natr_aut instead.")]
Notation Cnat_aut := mc_2_0.Cnat_aut (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intr_aut instead.")]
Notation Cint_aut := mc_2_0.Cint_aut (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use raddfZ_nat instead.")]
Notation raddfZ_Cnat := mc_2_0.raddfZ_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use raddfZ_int instead.")]
Notation raddfZ_Cint := mc_2_0.raddfZ_Cint (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use rpredZnat instead.")]
Notation rpredZ_Cnat := mc_2_0.rpredZ_Cnat (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use rpredZint instead.")]
Notation rpredZ_Cint := mc_2_0.rpredZ_Cint (only parsing).