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.cyclotomic.html | 39 ++++++++++++++--------------- 1 file changed, 19 insertions(+), 20 deletions(-) (limited to 'docs/htmldoc/mathcomp.field.cyclotomic.html') diff --git a/docs/htmldoc/mathcomp.field.cyclotomic.html b/docs/htmldoc/mathcomp.field.cyclotomic.html index aa91124..64a1afe 100644 --- a/docs/htmldoc/mathcomp.field.cyclotomic.html +++ b/docs/htmldoc/mathcomp.field.cyclotomic.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.

@@ -57,35 +56,35 @@
Definition cyclotomic (z : R) n :=
-  \prod_(k < n | coprime k n) ('X - (z ^+ k)%:P).
+  \prod_(k < n | coprime k n) ('X - (z ^+ k)%:P).

-Lemma cyclotomic_monic z n : cyclotomic z n \is monic.
+Lemma cyclotomic_monic z n : cyclotomic z n \is monic.

-Lemma size_cyclotomic z n : size (cyclotomic z n) = (totient n).+1.
+Lemma size_cyclotomic z n : size (cyclotomic z n) = (totient n).+1.

End Ring.

Lemma separable_Xn_sub_1 (R : idomainType) n :
-  n%:R != 0 :> R → @separable_poly R ('X^n - 1).
+  n%:R != 0 :> R → @separable_poly R ('X^n - 1).

Section Field.

-Variables (F : fieldType) (n : nat) (z : F).
-Hypothesis prim_z : n.-primitive_root z.
+Variables (F : fieldType) (n : nat) (z : F).
+Hypothesis prim_z : n.-primitive_root z.
Let n_gt0 := prim_order_gt0 prim_z.

-Lemma root_cyclotomic x : root (cyclotomic z n) x = n.-primitive_root x.
+Lemma root_cyclotomic x : root (cyclotomic z n) x = n.-primitive_root x.

Lemma prod_cyclotomic :
-  'X^n - 1 = \prod_(d <- divisors n) cyclotomic (z ^+ (n %/ d)) d.
+  'X^n - 1 = \prod_(d <- divisors n) cyclotomic (z ^+ (n %/ d)) d.

End Field.
@@ -98,10 +97,10 @@

-Local Hint Resolve (@intr_inj [numDomainType of algC]).
+Local Hint Resolve (@intr_inj [numDomainType of algC]) : core.

-Lemma C_prim_root_exists n : (n > 0)%N → {z : algC | n.-primitive_root z}.
+Lemma C_prim_root_exists n : (n > 0)%N → {z : algC | n.-primitive_root z}.

@@ -112,34 +111,34 @@

-Definition Cyclotomic n : {poly int} :=
-  let: exist z _ := C_prim_root_exists (ltn0Sn n.-1) in
+Definition Cyclotomic n : {poly int} :=
+  let: exist z _ := C_prim_root_exists (ltn0Sn n.-1) in
  map_poly floorC (cyclotomic z n).

-Notation "''Phi_' n" := (Cyclotomic n)
+Notation "''Phi_' n" := (Cyclotomic n)
  (at level 8, n at level 2, format "''Phi_' n").

-Lemma Cyclotomic_monic n : 'Phi_n \is monic.
+Lemma Cyclotomic_monic n : 'Phi_n \is monic.

Lemma Cintr_Cyclotomic n z :
-  n.-primitive_root z → pZtoC 'Phi_n = cyclotomic z n.
+  n.-primitive_root z → pZtoC 'Phi_n = cyclotomic z n.

Lemma prod_Cyclotomic n :
-  (n > 0)%N → \prod_(d <- divisors n) 'Phi_d = 'X^n - 1.
+  (n > 0)%N → \prod_(d <- divisors n) 'Phi_d = 'X^n - 1.

-Lemma Cyclotomic0 : 'Phi_0 = 1.
+Lemma Cyclotomic0 : 'Phi_0 = 1.

-Lemma size_Cyclotomic n : size 'Phi_n = (totient n).+1.
+Lemma size_Cyclotomic n : size 'Phi_n = (totient n).+1.

Lemma minCpoly_cyclotomic n z :
-  n.-primitive_root z → minCpoly z = cyclotomic z n.
+  n.-primitive_root z → minCpoly z = cyclotomic z n.
-- cgit v1.2.3