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.algebra.fraction.html | 187 ++++++++++++++-------------- 1 file changed, 93 insertions(+), 94 deletions(-) (limited to 'docs/htmldoc/mathcomp.algebra.fraction.html') diff --git a/docs/htmldoc/mathcomp.algebra.fraction.html b/docs/htmldoc/mathcomp.algebra.fraction.html index 2b78b50..745fa06 100644 --- a/docs/htmldoc/mathcomp.algebra.fraction.html +++ b/docs/htmldoc/mathcomp.algebra.fraction.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -58,58 +57,58 @@ ratios are pairs of R, such that the second member is nonzero
-Inductive ratio := mkRatio { frac :> R × R; _ : frac.2 != 0 }.
-Definition ratio_of of phant R := ratio.
+Inductive ratio := mkRatio { frac :> R × R; _ : frac.2 != 0 }.
+Definition ratio_of of phant R := ratio.

-Canonical ratio_subType := Eval hnf in [subType for frac].
-Canonical ratio_of_subType := Eval hnf in [subType of {ratio R}].
-Definition ratio_EqMixin := [eqMixin of ratio by <:].
+Canonical ratio_subType := Eval hnf in [subType for frac].
+Canonical ratio_of_subType := Eval hnf in [subType of {ratio R}].
+Definition ratio_EqMixin := [eqMixin of ratio by <:].
Canonical ratio_eqType := EqType ratio ratio_EqMixin.
-Canonical ratio_of_eqType := Eval hnf in [eqType of {ratio R}].
-Definition ratio_ChoiceMixin := [choiceMixin of ratio by <:].
+Canonical ratio_of_eqType := Eval hnf in [eqType of {ratio R}].
+Definition ratio_ChoiceMixin := [choiceMixin of ratio by <:].
Canonical ratio_choiceType := ChoiceType ratio ratio_ChoiceMixin.
-Canonical ratio_of_choiceType := Eval hnf in [choiceType of {ratio R}].
+Canonical ratio_of_choiceType := Eval hnf in [choiceType of {ratio R}].

-Lemma denom_ratioP : ∀ f : ratio, f.2 != 0.
+Lemma denom_ratioP : ∀ f : ratio, f.2 != 0.

-Definition ratio0 := (@mkRatio (0, 1) (oner_neq0 _)).
-Definition Ratio x y : {ratio R} := insubd ratio0 (x, y).
+Definition ratio0 := (@mkRatio (0, 1) (oner_neq0 _)).
+Definition Ratio x y : {ratio R} := insubd ratio0 (x, y).

-Lemma numer_Ratio x y : y != 0 → (Ratio x y).1 = x.
+Lemma numer_Ratio x y : y != 0 → (Ratio x y).1 = x.

-Lemma denom_Ratio x y : y != 0 → (Ratio x y).2 = y.
+Lemma denom_Ratio x y : y != 0 → (Ratio x y).2 = y.

-Definition numden_Ratio := (numer_Ratio, denom_Ratio).
+Definition numden_Ratio := (numer_Ratio, denom_Ratio).

-CoInductive Ratio_spec (n d : R) : {ratio R} → R → R → Type :=
-  | RatioNull of d = 0 : Ratio_spec n d ratio0 n 0
-  | RatioNonNull (d_neq0 : d != 0) :
-    Ratio_spec n d (@mkRatio (n, d) d_neq0) n d.
+Variant Ratio_spec (n d : R) : {ratio R} → R → R → Type :=
+  | RatioNull of d = 0 : Ratio_spec n d ratio0 n 0
+  | RatioNonNull (d_neq0 : d != 0) :
+    Ratio_spec n d (@mkRatio (n, d) d_neq0) n d.

Lemma RatioP n d : Ratio_spec n d (Ratio n d) n d.

-Lemma Ratio0 x : Ratio x 0 = ratio0.
+Lemma Ratio0 x : Ratio x 0 = ratio0.

End FracDomain.

-Notation "{ 'ratio' T }" := (ratio_of (Phant T)).
+Notation "{ 'ratio' T }" := (ratio_of (Phant T)).
Identity Coercion type_fracdomain_of : ratio_of >-> ratio.

-Notation "'\n_' x" := (frac x).1
+Notation "'\n_' x" := (frac x).1
  (at level 8, x at level 2, format "'\n_' x").
-Notation "'\d_' x" := (frac x).2
+Notation "'\d_' x" := (frac x).2
  (at level 8, x at level 2, format "'\d_' x").

@@ -134,16 +133,16 @@ Definition equivf x y := equivf_notation x y.

-Lemma equivfE x y : equivf x y = equivf_notation x y.
+Lemma equivfE x y : equivf x y = equivf_notation x y.

-Lemma equivf_refl : reflexive equivf.
+Lemma equivf_refl : reflexive equivf.

-Lemma equivf_sym : symmetric equivf.
+Lemma equivf_sym : symmetric equivf.

-Lemma equivf_trans : transitive equivf.
+Lemma equivf_trans : transitive equivf.

@@ -155,9 +154,9 @@ Canonical equivf_equiv := EquivRel equivf equivf_refl equivf_sym equivf_trans.

-Definition type := {eq_quot equivf}.
-Definition type_of of phant R := type.
-Notation "{ 'fraction' T }" := (type_of (Phant T)).
+Definition type := {eq_quot equivf}.
+Definition type_of of phant R := type.
+Notation "{ 'fraction' T }" := (type_of (Phant T)).

@@ -166,16 +165,16 @@ we recover some structure for the quotient
-Canonical frac_quotType := [quotType of type].
-Canonical frac_eqType := [eqType of type].
-Canonical frac_choiceType := [choiceType of type].
-Canonical frac_eqQuotType := [eqQuotType equivf of type].
+Canonical frac_quotType := [quotType of type].
+Canonical frac_eqType := [eqType of type].
+Canonical frac_choiceType := [choiceType of type].
+Canonical frac_eqQuotType := [eqQuotType equivf of type].

-Canonical frac_of_quotType := [quotType of {fraction R}].
-Canonical frac_of_eqType := [eqType of {fraction R}].
-Canonical frac_of_choiceType := [choiceType of {fraction R}].
-Canonical frac_of_eqQuotType := [eqQuotType equivf of {fraction R}].
+Canonical frac_of_quotType := [quotType of {fraction R}].
+Canonical frac_of_eqType := [eqType of {fraction R}].
+Canonical frac_of_choiceType := [choiceType of {fraction R}].
+Canonical frac_of_eqQuotType := [eqQuotType equivf of {fraction R}].

@@ -184,72 +183,72 @@ we explain what was the equivalence on the quotient
-Lemma equivf_def (x y : ratio R) : x == y %[mod type]
-                                    = (\n_x × \d_y == \d_x × \n_y).
+Lemma equivf_def (x y : ratio R) : x == y %[mod type]
+                                    = (\n_x × \d_y == \d_x × \n_y).

-Lemma equivf_r x : \n_x × \d_(repr (\pi_type x)) = \d_x × \n_(repr (\pi_type x)).
+Lemma equivf_r x : \n_x × \d_(repr (\pi_type x)) = \d_x × \n_(repr (\pi_type x)).

-Lemma equivf_l x : \n_(repr (\pi_type x)) × \d_x = \d_(repr (\pi_type x)) × \n_x.
+Lemma equivf_l x : \n_(repr (\pi_type x)) × \d_x = \d_(repr (\pi_type x)) × \n_x.

-Lemma numer0 x : (\n_x == 0) = (x == (ratio0 R) %[mod_eq equivf]).
+Lemma numer0 x : (\n_x == 0) = (x == (ratio0 R) %[mod_eq equivf]).

-Lemma Ratio_numden : ∀ x, Ratio \n_x \d_x = x.
+Lemma Ratio_numden : ∀ x, Ratio \n_x \d_x = x.

-Definition tofrac := lift_embed {fraction R} (fun x : R ⇒ Ratio x 1).
+Definition tofrac := lift_embed {fraction R} (fun x : R ⇒ Ratio x 1).
Canonical tofrac_pi_morph := PiEmbed tofrac.

-Notation "x %:F" := (@tofrac x).
+Notation "x %:F" := (@tofrac x).

Implicit Types a b c : type.

-Definition addf x y : dom := Ratio (\n_x × \d_y + \n_y × \d_x) (\d_x × \d_y).
-Definition add := lift_op2 {fraction R} addf.
+Definition addf x y : dom := Ratio (\n_x × \d_y + \n_y × \d_x) (\d_x × \d_y).
+Definition add := lift_op2 {fraction R} addf.

-Lemma pi_add : {morph \pi : x y / addf x y >-> add x y}.
+Lemma pi_add : {morph \pi : x y / addf x y >-> add x y}.
Canonical pi_add_morph := PiMorph2 pi_add.

-Definition oppf x : dom := Ratio (- \n_x) \d_x.
-Definition opp := lift_op1 {fraction R} oppf.
-Lemma pi_opp : {morph \pi : x / oppf x >-> opp x}.
+Definition oppf x : dom := Ratio (- \n_x) \d_x.
+Definition opp := lift_op1 {fraction R} oppf.
+Lemma pi_opp : {morph \pi : x / oppf x >-> opp x}.
Canonical pi_opp_morph := PiMorph1 pi_opp.

-Definition mulf x y : dom := Ratio (\n_x × \n_y) (\d_x × \d_y).
-Definition mul := lift_op2 {fraction R} mulf.
+Definition mulf x y : dom := Ratio (\n_x × \n_y) (\d_x × \d_y).
+Definition mul := lift_op2 {fraction R} mulf.

-Lemma pi_mul : {morph \pi : x y / mulf x y >-> mul x y}.
+Lemma pi_mul : {morph \pi : x y / mulf x y >-> mul x y}.
Canonical pi_mul_morph := PiMorph2 pi_mul.

-Definition invf x : dom := Ratio \d_x \n_x.
-Definition inv := lift_op1 {fraction R} invf.
+Definition invf x : dom := Ratio \d_x \n_x.
+Definition inv := lift_op1 {fraction R} invf.

-Lemma pi_inv : {morph \pi : x / invf x >-> inv x}.
+Lemma pi_inv : {morph \pi : x / invf x >-> inv x}.
Canonical pi_inv_morph := PiMorph1 pi_inv.

-Lemma addA : associative add.
+Lemma addA : associative add.

-Lemma addC : commutative add.
+Lemma addC : commutative add.

-Lemma add0_l : left_id 0%:F add.
+Lemma add0_l : left_id 0%:F add.

-Lemma addN_l : left_inverse 0%:F opp add.
+Lemma addN_l : left_inverse 0%:F opp add.

@@ -262,19 +261,19 @@ Canonical frac_zmodType := Eval hnf in ZmodType type frac_zmodMixin.

-Lemma mulA : associative mul.
+Lemma mulA : associative mul.

-Lemma mulC : commutative mul.
+Lemma mulC : commutative mul.

-Lemma mul1_l : left_id 1%:F mul.
+Lemma mul1_l : left_id 1%:F mul.

-Lemma mul_addl : left_distributive mul add.
+Lemma mul_addl : left_distributive mul add.

-Lemma nonzero1 : 1%:F != 0%:F :> type.
+Lemma nonzero1 : 1%:F != 0%:F :> type.

@@ -288,10 +287,10 @@ Canonical frac_comRingType := Eval hnf in ComRingType type mulC.

-Lemma mulV_l : ∀ a, a != 0%:F → mul (inv a) a = 1%:F.
+Lemma mulV_l : ∀ a, a != 0%:F → mul (inv a) a = 1%:F.

-Lemma inv0 : inv 0%:F = 0%:F.
+Lemma inv0 : inv 0%:F = 0%:F.

@@ -302,7 +301,7 @@
Definition RatFieldUnitMixin := FieldUnitMixin mulV_l inv0.
Canonical frac_unitRingType := Eval hnf in UnitRingType type RatFieldUnitMixin.
-Canonical frac_comUnitRingType := [comUnitRingType of type].
+Canonical frac_comUnitRingType := [comUnitRingType of type].

Lemma field_axiom : GRing.Field.mixin_of frac_unitRingType.
@@ -324,9 +323,9 @@ End FracField.

-Notation "{ 'fraction' T }" := (FracField.type_of (Phant T)).
+Notation "{ 'fraction' T }" := (FracField.type_of (Phant T)).
Notation equivf := (@FracField.equivf _).
-Hint Resolve denom_ratioP.
+Hint Resolve denom_ratioP : core.

Section Canonicals.
@@ -352,16 +351,16 @@ Canonical FracField.frac_idomainType.
Canonical FracField.frac_fieldType.
Canonical FracField.tofrac_pi_morph.
-Canonical frac_of_quotType := Eval hnf in [quotType of {fraction R}].
-Canonical frac_of_eqType := Eval hnf in [eqType of {fraction R}].
-Canonical frac_of_choiceType := Eval hnf in [choiceType of {fraction R}].
-Canonical frac_of_zmodType := Eval hnf in [zmodType of {fraction R}].
-Canonical frac_of_ringType := Eval hnf in [ringType of {fraction R}].
-Canonical frac_of_comRingType := Eval hnf in [comRingType of {fraction R}].
-Canonical frac_of_unitRingType := Eval hnf in [unitRingType of {fraction R}].
-Canonical frac_of_comUnitRingType := Eval hnf in [comUnitRingType of {fraction R}].
-Canonical frac_of_idomainType := Eval hnf in [idomainType of {fraction R}].
-Canonical frac_of_fieldType := Eval hnf in [fieldType of {fraction R}].
+Canonical frac_of_quotType := Eval hnf in [quotType of {fraction R}].
+Canonical frac_of_eqType := Eval hnf in [eqType of {fraction R}].
+Canonical frac_of_choiceType := Eval hnf in [choiceType of {fraction R}].
+Canonical frac_of_zmodType := Eval hnf in [zmodType of {fraction R}].
+Canonical frac_of_ringType := Eval hnf in [ringType of {fraction R}].
+Canonical frac_of_comRingType := Eval hnf in [comRingType of {fraction R}].
+Canonical frac_of_unitRingType := Eval hnf in [unitRingType of {fraction R}].
+Canonical frac_of_comUnitRingType := Eval hnf in [comUnitRingType of {fraction R}].
+Canonical frac_of_idomainType := Eval hnf in [idomainType of {fraction R}].
+Canonical frac_of_fieldType := Eval hnf in [fieldType of {fraction R}].

End Canonicals.
@@ -376,7 +375,7 @@ Variable R : idomainType.

-Lemma Ratio_numden (x : {ratio R}) : Ratio \n_x \d_x = x.
+Lemma Ratio_numden (x : {ratio R}) : Ratio \n_x \d_x = x.

@@ -405,21 +404,21 @@ tests
-Lemma tofrac0 : 0%:F = 0.
-Lemma tofracN : {morph tofrac: x / - x}.
-Lemma tofracD : {morph tofrac: x y / x + y}.
-Lemma tofracB : {morph tofrac: x y / x - y}.
-Lemma tofracMn n : {morph tofrac: x / x *+ n}.
-Lemma tofracMNn n : {morph tofrac: x / x *- n}.
-Lemma tofrac1 : 1%:F = 1.
-Lemma tofracM : {morph tofrac: x y / x × y}.
-Lemma tofracX n : {morph tofrac: x / x ^+ n}.
+Lemma tofrac0 : 0%:F = 0.
+Lemma tofracN : {morph tofrac: x / - x}.
+Lemma tofracD : {morph tofrac: x y / x + y}.
+Lemma tofracB : {morph tofrac: x y / x - y}.
+Lemma tofracMn n : {morph tofrac: x / x *+ n}.
+Lemma tofracMNn n : {morph tofrac: x / x *- n}.
+Lemma tofrac1 : 1%:F = 1.
+Lemma tofracM : {morph tofrac: x y / x × y}.
+Lemma tofracX n : {morph tofrac: x / x ^+ n}.

-Lemma tofrac_eq (p q : R): (p%:F == q%:F) = (p == q).
+Lemma tofrac_eq (p q : R): (p%:F == q%:F) = (p == q).

-Lemma tofrac_eq0 (p : R): (p%:F == 0) = (p == 0).
+Lemma tofrac_eq0 (p : R): (p%:F == 0) = (p == 0).
End FracFieldTheory.
-- cgit v1.2.3