From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.field.algC.html | 478 +++++++++++++++++-----------------
1 file changed, 244 insertions(+), 234 deletions(-)
(limited to 'docs/htmldoc/mathcomp.field.algC.html')
diff --git a/docs/htmldoc/mathcomp.field.algC.html b/docs/htmldoc/mathcomp.field.algC.html
index 4449509..5ab5e5d 100644
--- a/docs/htmldoc/mathcomp.field.algC.html
+++ b/docs/htmldoc/mathcomp.field.algC.html
@@ -21,7 +21,6 @@
@@ -85,9 +84,9 @@
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}.
+
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.
@@ -113,21 +112,21 @@
Parameter zmodMixin :
GRing.Zmodule.mixin_of type.
Canonical zmodType :=
ZmodType type zmodMixin.
-
Canonical countZmodType :=
[countZmodType of type].
+
Canonical countZmodType :=
[countZmodType of type].
Parameter ringMixin :
GRing.Ring.mixin_of zmodType.
Canonical ringType :=
RingType type ringMixin.
-
Canonical countRingType :=
[countRingType of type].
+
Canonical countRingType :=
[countRingType of type].
Parameter unitRingMixin :
GRing.UnitRing.mixin_of ringType.
Canonical unitRingType :=
UnitRingType type unitRingMixin.
-
Axiom mulC : @
commutative ringType ringType *%R.
+
Axiom mulC : @
commutative ringType ringType *%R.
Canonical comRingType :=
ComRingType type mulC.
-
Canonical comUnitRingType :=
[comUnitRingType of type].
+
Canonical comUnitRingType :=
[comUnitRingType of type].
Axiom idomainAxiom :
GRing.IntegralDomain.axiom ringType.
@@ -148,7 +147,7 @@
Parameter numMixin :
Num.mixin_of ringType.
Canonical numDomainType :=
NumDomainType type numMixin.
-
Canonical numFieldType :=
[numFieldType of type].
+
Canonical numFieldType :=
[numFieldType of type].
Parameter conjMixin :
Num.ClosedField.imaginary_mixin_of numDomainType.
@@ -164,36 +163,36 @@
Module Implementation :
Specification.
-
Definition L :=
tag Fundamental_Theorem_of_Algebraics.
+
Definition L :=
tag Fundamental_Theorem_of_Algebraics.
-
Definition conjL :
{rmorphism L → L} :=
-
s2val (
tagged Fundamental_Theorem_of_Algebraics).
+
Definition conjL :
{rmorphism L → L} :=
+
s2val (
tagged Fundamental_Theorem_of_Algebraics).
-
Fact conjL_K :
involutive conjL.
+
Fact conjL_K :
involutive conjL.
-
Fact conjL_nt :
¬ conjL =1 id.
+
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]].
+
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.
+
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.
+
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 type :
Type :=
{eq_quot eq_root}%
qT.
Definition eqMixin :
Equality.class_of type :=
EquivQuot.eqMixin _.
@@ -204,27 +203,27 @@
Canonical choiceType :=
ChoiceType type choiceMixin.
-
Definition countMixin :
Countable.mixin_of type :=
CanCountMixin (@
reprK _ _).
+
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_inj :
injective CtoL.
Fact CtoL_P u :
integralOver QtoL (
CtoL u).
-
Fact LtoC_subproof z :
integralOver QtoL z → {u | CtoL u = z}.
+
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 LtoC_K z Az :
CtoL (@
LtoC z Az)
= z.
-
Fact CtoL_K u :
LtoC (
CtoL_P u)
= u.
+
Fact CtoL_K u :
LtoC (
CtoL_P u)
= u.
Definition zero :=
LtoC (
integral0 _).
@@ -232,21 +231,21 @@
Definition opp u :=
LtoC (
integral_opp (
CtoL_P u)).
-
Fact addA :
associative add.
+
Fact addA :
associative add.
-
Fact addC :
commutative add.
+
Fact addC :
commutative add.
-
Fact add0 :
left_id zero add.
+
Fact add0 :
left_id zero add.
-
Fact addN :
left_inverse zero opp 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].
+
Canonical countZmodType :=
[countZmodType of type].
Fact CtoL_is_additive :
additive CtoL.
@@ -258,25 +257,25 @@
Definition inv u :=
LtoC (
integral_inv (
CtoL_P u)).
-
Fact mulA :
associative mul.
+
Fact mulA :
associative mul.
-
Fact mulC :
commutative mul.
+
Fact mulC :
commutative mul.
-
Fact mul1 :
left_id one mul.
+
Fact mul1 :
left_id one mul.
-
Fact mulD :
left_distributive mul +%R.
+
Fact mulD :
left_distributive mul +%R.
-
Fact one_nz :
one != 0
:> type.
+
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].
+
Canonical countRingType :=
[countRingType of type].
Fact CtoL_is_multiplicative :
multiplicative CtoL.
@@ -284,15 +283,15 @@
Fact mulVf :
GRing.Field.axiom inv.
-
Fact inv0 :
inv 0
= 0.
+
Fact inv0 :
inv 0
= 0.
Definition unitRingMixin :=
FieldUnitMixin mulVf inv0.
Canonical unitRingType :=
UnitRingType type unitRingMixin.
-
Canonical comUnitRingType :=
[comUnitRingType of type].
+
Canonical comUnitRingType :=
[comUnitRingType of type].
-
Definition fieldMixin := @
FieldMixin _ _ mulVf inv0.
+
Definition fieldMixin :=
FieldMixin mulVf inv0.
Definition idomainAxiom :=
FieldIdomainMixin fieldMixin.
Canonical idomainType :=
IdomainType type idomainAxiom.
Canonical fieldType :=
FieldType type fieldMixin.
@@ -301,26 +300,26 @@
Fact closedFieldAxiom :
GRing.ClosedField.axiom ringType.
-
Definition decFieldMixin :=
closed_field.closed_fields_QEMixin closedFieldAxiom.
+
Definition decFieldMixin :=
closed_field_QEMixin closedFieldAxiom.
Canonical decFieldType :=
DecFieldType type decFieldMixin.
Canonical closedFieldType :=
ClosedFieldType type closedFieldAxiom.
Fact conj_subproof u :
integralOver QtoL (
conjL (
CtoL u)).
Fact conj_is_rmorphism :
rmorphism (
fun u ⇒
LtoC (
conj_subproof u)).
-
Definition conj :
{rmorphism type → type} :=
RMorphism conj_is_rmorphism.
-
Lemma conjK :
involutive conj.
+
Definition conj :
{rmorphism type → type} :=
RMorphism conj_is_rmorphism.
+
Lemma conjK :
involutive conj.
-
Fact conj_nt :
¬ conj =1 id.
+
Fact conj_nt :
¬ conj =1 id.
Definition numMixin :=
sval (
ComplexNumMixin conjK conj_nt).
Canonical numDomainType :=
NumDomainType type numMixin.
-
Canonical numFieldType :=
[numFieldType of type].
+
Canonical numFieldType :=
[numFieldType of type].
-
Lemma normK u :
`|u| ^+ 2
= u × conj u.
+
Lemma normK u :
`|u| ^+ 2
= u × conj u.
Lemma algebraic :
integralRange (@
ratr unitRingType).
@@ -328,7 +327,7 @@
Definition conjMixin :=
ImaginaryMixin (
svalP (
imaginary_exists closedFieldType))
- (
fun x ⇒
esym (
normK x)).
+ (
fun x ⇒
esym (
normK x)).
Canonical numClosedFieldType :=
NumClosedFieldType type conjMixin.
@@ -346,25 +345,25 @@
-
Fact algCi_subproof :
{i : algC | i ^+ 2
= -1
}.
+
Fact algCi_subproof :
{i : algC | i ^+ 2
= -1
}.
-
CoInductive getCrat_spec :
Type :=
GetCrat_spec CtoQ of cancel QtoC CtoQ.
+
Variant getCrat_spec :
Type :=
GetCrat_spec CtoQ of cancel QtoC CtoQ.
Fact getCrat_subproof :
getCrat_spec.
-
Fact floorC_subproof x :
{m | x \is Creal → ZtoC m ≤ x < ZtoC (
m + 1)
}.
+
Fact 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}.
+
{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.
+
Definition algC_divisor (
x :
algC) :=
x : divisor.
+
Definition int_divisor m :=
m%:~R : divisor.
+
Definition nat_divisor n :=
n%:R : divisor.
End Internals.
@@ -416,19 +415,19 @@
Definition getCrat :=
let:
GetCrat_spec CtoQ _ :=
getCrat_subproof in CtoQ.
-
Definition Crat :
pred_class :=
fun x :
algC ⇒
ratr (
getCrat x)
== x.
+
Definition Crat :
{pred algC} :=
fun x ⇒
ratr (
getCrat x)
== x.
Definition floorC x :=
sval (
floorC_subproof x).
-
Definition Cint :
pred_class :=
fun x :
algC ⇒
(floorC x)%:~R == x.
+
Definition Cint :
{pred algC} :=
fun x ⇒
(floorC x)%:~R == x.
-
Definition truncC x :=
if x ≥ 0
then `|floorC x|%
N else 0%
N.
-
Definition Cnat :
pred_class :=
fun x :
algC ⇒
(truncC x)%:R == x.
+
Definition truncC x :=
if x ≥ 0
then `|floorC x|%
N else 0%
N.
+
Definition Cnat :
{pred algC} :=
fun x ⇒
(truncC x)%:R == x.
-
Definition minCpoly x :
{poly algC} :=
-
let:
exist2 p _ _ :=
minCpoly_subproof x in map_poly ratr p.
+
Definition minCpoly x :
{poly algC} :=
+
let:
exist2 p _ _ :=
minCpoly_subproof x in map_poly ratr p.
Coercion nat_divisor : nat >-> divisor.
@@ -436,22 +435,22 @@
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).
+
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 dvdC (
x :
divisor) :
{pred algC} :=
+
fun y ⇒
if x == 0
then y == 0
else y / x \in Cint.
+
Notation "x %| y" := (
y \in dvdC x) :
C_expanded_scope.
+
Notation "x %| y" := (@
in_mem divisor y (
mem (
dvdC x))) :
C_scope.
-
Definition eqCmod (
e x y :
divisor) := (
e %| x - y)%
C.
+
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.
+
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.
@@ -466,11 +465,13 @@
Section AlgebraicsTheory.
-
Implicit Types (
x y z :
algC) (
n :
nat) (
m :
int) (
b :
bool).
+
Implicit Types (
x y z :
algC) (
n :
nat) (
m :
int) (
b :
bool).
Import Algebraics.Internals.
-
Local Hint Resolve (@
intr_inj _ : injective ZtoC).
+
+
+
Local Hint Resolve (
intr_inj : injective ZtoC) :
core.
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)))).
+ ((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)))).
+ ((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 nz2 : 2%:R != 0 :> algC.
@@ -535,19 +536,25 @@
+
+
+ Trivial cannot resolve a general real0 hint.
+
+
@@ -559,61 +566,62 @@
-
Lemma floorC_itv x :
x \is Creal → (floorC x)%:~R ≤ x < (floorC x + 1
)%:~R.
+
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 floorC_def x m :
m%:~R ≤ x < (m + 1
)%:~R → floorC x = m.
-
Lemma intCK :
cancel intr floorC.
+
Lemma intCK :
cancel intr floorC.
-
Lemma floorCK :
{in Cint, cancel floorC intr}.
+
Lemma floorCK :
{in Cint, cancel floorC intr}.
-
Lemma floorC0 :
floorC 0
= 0.
-
Lemma floorC1 :
floorC 1
= 1.
-
Hint Resolve floorC0 floorC1.
+
Lemma floorC0 :
floorC 0
= 0.
+
Lemma floorC1 :
floorC 1
= 1.
+
Hint Resolve floorC0 floorC1 :
core.
-
Lemma floorCpK (
p :
{poly algC}) :
-
p \is a polyOver Cint → map_poly intr (
map_poly floorC p)
= p.
+
Lemma 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 floorCpP (
p :
{poly algC}) :
+
p \is a polyOver Cint → {q | p = map_poly intr q}.
-
Lemma Cint_int m :
m%:~R \in Cint.
+
Lemma Cint_int m :
m%:~R \in Cint.
-
Lemma CintP x :
reflect (
∃ m, x = m%:~R) (
x \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 floorCD :
{in Cint & Creal, {morph floorC : x y / x + y}}.
-
Lemma floorCN :
{in Cint, {morph floorC : x / - x}}.
+
Lemma floorCN :
{in Cint, {morph floorC : x / - x}}.
-
Lemma floorCM :
{in Cint &, {morph floorC : x y / x × y}}.
+
Lemma floorCM :
{in Cint &, {morph floorC : x y / x × y}}.
-
Lemma floorCX n :
{in Cint, {morph floorC : x / x ^+ n}}.
+
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 rpred_Cint
+ (
S :
{pred algC}) (
ringS :
subringPred S) (
kS :
keyed_pred ringS)
x :
+
x \in Cint → x \in kS.
-
Lemma Cint0 : 0
\in Cint.
-
Lemma Cint1 : 1
\in Cint.
-
Hint Resolve Cint0 Cint1.
+
Lemma Cint0 : 0
\in Cint.
+
Lemma Cint1 : 1
\in Cint.
+
Hint Resolve Cint0 Cint1 :
core.
-
Fact Cint_key :
pred_key Cint.
+
Fact Cint_key :
pred_key Cint.
Fact Cint_subring :
subring_closed Cint.
-
Canonical Cint_keyed :=
KeyedPred Cint_key.
+
Canonical Cint_keyed :=
KeyedPred Cint_key.
Canonical Cint_opprPred :=
OpprPred Cint_subring.
Canonical Cint_addrPred :=
AddrPred Cint_subring.
Canonical Cint_mulrPred :=
MulrPred Cint_subring.
@@ -623,16 +631,16 @@
Canonical Cint_subringPred :=
SubringPred Cint_subring.
-
Lemma Creal_Cint :
{subset Cint ≤ Creal}.
+
Lemma Creal_Cint :
{subset Cint ≤ Creal}.
-
Lemma conj_Cint x :
x \in Cint → x^* = x.
+
Lemma conj_Cint x :
x \in Cint → x^* = x.
-
Lemma Cint_normK x :
x \in Cint → `|x| ^+ 2
= x ^+ 2.
+
Lemma Cint_normK x :
x \in Cint → `|x| ^+ 2
= x ^+ 2.
-
Lemma CintEsign x :
x \in Cint → x = (-1
) ^+ (
x < 0)%
C × `|x|.
+
Lemma CintEsign x :
x \in Cint → x = (-1
) ^+ (
x < 0)%
C × `|x|.
@@ -643,86 +651,87 @@
-
Lemma truncC_itv x : 0
≤ x → (truncC x)%:R ≤ x < (truncC x).+1%:R.
+
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 truncC_def x n :
n%:R ≤ x < n.+1%:R → truncC x = n.
-
Lemma natCK n :
truncC n%:R = n.
+
Lemma natCK n :
truncC n%:R = n.
-
Lemma CnatP x :
reflect (
∃ n, x = n%:R) (
x \in Cnat).
+
Lemma CnatP x :
reflect (
∃ n, x = n%:R) (
x \in Cnat).
-
Lemma truncCK :
{in Cnat, cancel truncC (
GRing.natmul 1)
}.
+
Lemma truncCK :
{in Cnat, cancel truncC (
GRing.natmul 1)
}.
-
Lemma truncC_gt0 x : (0
< truncC x)%
N = (1
≤ x).
+
Lemma truncC_gt0 x : (0
< truncC x)%
N = (1
≤ x).
-
Lemma truncC0Pn x :
reflect (
truncC x = 0%
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 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}}.
+
{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 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 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 rpred_Cnat
+ (
S :
{pred algC}) (
ringS :
semiringPred S) (
kS :
keyed_pred ringS)
x :
+
x \in Cnat → x \in kS.
-
Lemma Cnat_nat n :
n%:R \in Cnat.
-
Lemma Cnat0 : 0
\in Cnat.
-
Lemma Cnat1 : 1
\in Cnat.
-
Hint Resolve Cnat_nat Cnat0 Cnat1.
+
Lemma Cnat_nat n :
n%:R \in Cnat.
+
Lemma Cnat0 : 0
\in Cnat.
+
Lemma Cnat1 : 1
\in Cnat.
+
Hint Resolve Cnat_nat Cnat0 Cnat1 :
core.
-
Fact Cnat_key :
pred_key Cnat.
+
Fact Cnat_key :
pred_key Cnat.
Fact Cnat_semiring :
semiring_closed Cnat.
-
Canonical Cnat_keyed :=
KeyedPred Cnat_key.
+
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_ge0 x :
x \in Cnat → 0
≤ x.
-
Lemma Cnat_gt0 x :
x \in Cnat → (0
< x) = (x != 0
).
+
Lemma Cnat_gt0 x :
x \in Cnat → (0
< x) = (x != 0
).
-
Lemma conj_Cnat x :
x \in Cnat → x^* = x.
+
Lemma conj_Cnat x :
x \in Cnat → x^* = x.
-
Lemma norm_Cnat x :
x \in Cnat → `|x| = x.
+
Lemma norm_Cnat x :
x \in Cnat → `|x| = x.
-
Lemma Creal_Cnat :
{subset Cnat ≤ Creal}.
+
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_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
).
+
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 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.
@@ -733,31 +742,31 @@
@@ -768,49 +777,49 @@
@@ -821,69 +830,69 @@
-
Lemma eqCmod_refl e x : (
x == x %[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 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 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_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.
+ (
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.
+ (
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.
+ (
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 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 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 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.
+ (
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 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 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.
+
{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.
+
{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 eqCmodMl0 e :
{in Cint, ∀ x,
x × e == 0
%[mod e]}%
C.
-
Lemma eqCmodMr0 e :
{in Cint, ∀ x,
e × x == 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 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 eqCmodM e :
{in Cint & Cint, ∀ x1 y2 x2 y1,
+
x1 == x2 %[mod e] → y1 == y2 %[mod e] → x1 × y1 == x2 × y2 %[mod e]}%
C.
@@ -894,26 +903,26 @@
@@ -965,35 +975,35 @@
Section AutC.
-Implicit Type nu : {rmorphism algC → algC}.
+Implicit Type nu : {rmorphism algC → algC}.
-Lemma aut_Cnat nu : {in Cnat, nu =1 id}.
+Lemma aut_Cnat nu : {in Cnat, nu =1 id}.
-Lemma aut_Cint nu : {in Cint, nu =1 id}.
+Lemma aut_Cint nu : {in Cint, nu =1 id}.
-Lemma aut_Crat nu : {in Crat, 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 Cnat_aut nu x : (nu x \in Cnat) = (x \in Cnat).
-Lemma Cint_aut nu x : (nu x \in Cint) = (x \in Cint).
+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 Crat_aut nu x : (nu x \in Crat) = (x \in Crat).
-Lemma algC_invaut_subproof nu x : {y | nu y = x}.
+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_invautK nu : cancel (algC_invaut nu) nu.
-Lemma algC_autK nu : cancel nu (algC_invaut nu).
+Lemma algC_autK nu : cancel nu (algC_invaut nu).
Fact algC_invaut_is_rmorphism nu : rmorphism (algC_invaut nu).
@@ -1001,7 +1011,7 @@
Canonical algC_invaut_rmorphism nu := RMorphism (algC_invaut_is_rmorphism nu).
-Lemma minCpoly_aut nu x : minCpoly (nu x) = minCpoly x.
+Lemma minCpoly_aut nu x : minCpoly (nu x) = minCpoly x.
End AutC.
@@ -1010,13 +1020,13 @@
Section AutLmodC.
-Variables (U V : lmodType algC) (f : {additive U → V}).
+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_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.
+Lemma raddfZ_Cint a u : a \in Cint → f (a *: u) = a *: f u.
End AutLmodC.
@@ -1028,20 +1038,20 @@
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_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}.
+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.
+Hint Resolve Creal0 Creal1 Cnat_nat Cnat0 Cnat1 Cint0 Cint1 floorC0 Crat0 Crat1 : core.
+Hint Resolve dvdC0 dvdC_refl eqCmod_refl eqCmodm0 : core.
--
cgit v1.2.3