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.solvable.cyclic.html | 243 ++++++++++++++--------------- 1 file changed, 121 insertions(+), 122 deletions(-) (limited to 'docs/htmldoc/mathcomp.solvable.cyclic.html') diff --git a/docs/htmldoc/mathcomp.solvable.cyclic.html b/docs/htmldoc/mathcomp.solvable.cyclic.html index 858273d..731109c 100644 --- a/docs/htmldoc/mathcomp.solvable.cyclic.html +++ b/docs/htmldoc/mathcomp.solvable.cyclic.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.

@@ -74,19 +73,19 @@
Variable gT : finGroupType.
-Implicit Types (a x y : gT) (A B : {set gT}) (G K H : {group gT}).
+Implicit Types (a x y : gT) (A B : {set gT}) (G K H : {group gT}).

-Definition cyclic A := [∃ x, A == <[x]>].
+Definition cyclic A := [∃ x, A == <[x]>].

-Lemma cyclicP A : reflect (∃ x, A = <[x]>) (cyclic A).
+Lemma cyclicP A : reflect (∃ x, A = <[x]>) (cyclic A).

-Lemma cycle_cyclic x : cyclic <[x]>.
+Lemma cycle_cyclic x : cyclic <[x]>.

-Lemma cyclic1 : cyclic [1 gT].
+Lemma cyclic1 : cyclic [1 gT].

@@ -103,28 +102,28 @@ Variable a : gT.

-Definition Zpm (i : 'Z_#[a]) := a ^+ i.
+Definition Zpm (i : 'Z_#[a]) := a ^+ i.

-Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x × y}}.
+Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x × y}}.

Canonical Zpm_morphism := Morphism ZpmM.

-Lemma im_Zpm : Zpm @* Zp #[a] = <[a]>.
+Lemma im_Zpm : Zpm @* Zp #[a] = <[a]>.

-Lemma injm_Zpm : 'injm Zpm.
+Lemma injm_Zpm : 'injm Zpm.

-Lemma eq_expg_mod_order m n : (a ^+ m == a ^+ n) = (m == n %[mod #[a]]).
+Lemma eq_expg_mod_order m n : (a ^+ m == a ^+ n) = (m == n %[mod #[a]]).

-Lemma Zp_isom : isom (Zp #[a]) <[a]> Zpm.
+Lemma Zp_isom : isom (Zp #[a]) <[a]> Zpm.

-Lemma Zp_isog : isog (Zp #[a]) <[a]>.
+Lemma Zp_isog : isog (Zp #[a]) <[a]>.

End Zpm.
@@ -138,25 +137,25 @@

-Lemma cyclic_abelian A : cyclic A → abelian A.
+Lemma cyclic_abelian A : cyclic A → abelian A.

Lemma cycleMsub a b :
-  commute a b → coprime #[a] #[b] → <[a]> \subset <[a × b]>.
+  commute a b → coprime #[a] #[b] → <[a]> \subset <[a × b]>.

Lemma cycleM a b :
-  commute a b → coprime #[a] #[b] → <[a × b]> = <[a]> × <[b]>.
+  commute a b → coprime #[a] #[b] → <[a × b]> = <[a]> × <[b]>.

Lemma cyclicM A B :
-    cyclic A → cyclic B → B \subset 'C(A) → coprime #|A| #|B| →
-  cyclic (A × B).
+    cyclic A → cyclic B → B \subset 'C(A) → coprime #|A| #|B| →
+  cyclic (A × B).

Lemma cyclicY K H :
-    cyclic K → cyclic H → H \subset 'C(K) → coprime #|K| #|H| →
-  cyclic (K <*> H).
+    cyclic K → cyclic H → H \subset 'C(K) → coprime #|K| #|H| →
+  cyclic (K <*> H).

@@ -167,66 +166,66 @@

-Lemma order_dvdn a n : #[a] %| n = (a ^+ n == 1).
+Lemma order_dvdn a n : #[a] %| n = (a ^+ n == 1).

-Lemma order_inf a n : a ^+ n.+1 == 1 → #[a] ≤ n.+1.
+Lemma order_inf a n : a ^+ n.+1 == 1 → #[a] ≤ n.+1.

-Lemma order_dvdG G a : a \in G → #[a] %| #|G|.
+Lemma order_dvdG G a : a \in G → #[a] %| #|G|.

-Lemma expg_cardG G a : a \in G → a ^+ #|G| = 1.
+Lemma expg_cardG G a : a \in G → a ^+ #|G| = 1.

-Lemma expg_znat G x k : x \in G → x ^+ (k%:R : 'Z_(#|G|))%R = x ^+ k.
+Lemma expg_znat G x k : x \in G → x ^+ (k%:R : 'Z_(#|G|))%R = x ^+ k.

-Lemma expg_zneg G x (k : 'Z_(#|G|)) : x \in G → x ^+ (- k)%R = x ^- k.
+Lemma expg_zneg G x (k : 'Z_(#|G|)) : x \in G → x ^+ (- k)%R = x ^- k.

-Lemma nt_gen_prime G x : prime #|G| → x \in G^# → G :=: <[x]>.
+Lemma nt_gen_prime G x : prime #|G| → x \in G^# → G :=: <[x]>.

-Lemma nt_prime_order p x : prime p → x ^+ p = 1 → x != 1 → #[x] = p.
+Lemma nt_prime_order p x : prime p → x ^+ p = 1 → x != 1 → #[x] = p.

-Lemma orderXdvd a n : #[a ^+ n] %| #[a].
+Lemma orderXdvd a n : #[a ^+ n] %| #[a].

-Lemma orderXgcd a n : #[a ^+ n] = #[a] %/ gcdn #[a] n.
+Lemma orderXgcd a n : #[a ^+ n] = #[a] %/ gcdn #[a] n.

-Lemma orderXdiv a n : n %| #[a] → #[a ^+ n] = #[a] %/ n.
+Lemma orderXdiv a n : n %| #[a] → #[a ^+ n] = #[a] %/ n.

-Lemma orderXexp p m n x : #[x] = (p ^ n)%N → #[x ^+ (p ^ m)] = (p ^ (n - m))%N.
+Lemma orderXexp p m n x : #[x] = (p ^ n)%N → #[x ^+ (p ^ m)] = (p ^ (n - m))%N.

Lemma orderXpfactor p k n x :
-  #[x ^+ (p ^ k)] = n → prime p → p %| n → #[x] = (p ^ k × n)%N.
+  #[x ^+ (p ^ k)] = n → prime p → p %| n → #[x] = (p ^ k × n)%N.

Lemma orderXprime p n x :
-  #[x ^+ p] = n → prime p → p %| n → #[x] = (p × n)%N.
+  #[x ^+ p] = n → prime p → p %| n → #[x] = (p × n)%N.

-Lemma orderXpnat m n x : #[x ^+ m] = n → \pi(n).-nat m → #[x] = (m × n)%N.
+Lemma orderXpnat m n x : #[x ^+ m] = n → \pi(n).-nat m → #[x] = (m × n)%N.

Lemma orderM a b :
-  commute a b → coprime #[a] #[b] → #[a × b] = (#[a] × #[b])%N.
+  commute a b → coprime #[a] #[b] → #[a × b] = (#[a] × #[b])%N.

-Definition expg_invn A k := (egcdn k #|A|).1.
+Definition expg_invn A k := (egcdn k #|A|).1.

Lemma expgK G k :
-  coprime #|G| k → {in G, cancel (expgn^~ k) (expgn^~ (expg_invn G k))}.
+  coprime #|G| k → {in G, cancel (expgn^~ k) (expgn^~ (expg_invn G k))}.

Lemma cyclic_dprod K H G :
-  K \x H = G → cyclic K → cyclic H → cyclic G = coprime #|K| #|H| .
+  K \x H = G → cyclic K → cyclic H → cyclic G = coprime #|K| #|H| .

@@ -237,16 +236,16 @@

-Definition generator (A : {set gT}) a := A == <[a]>.
+Definition generator (A : {set gT}) a := A == <[a]>.

-Lemma generator_cycle a : generator <[a]> a.
+Lemma generator_cycle a : generator <[a]> a.

-Lemma cycle_generator a x : generator <[a]> x → x \in <[a]>.
+Lemma cycle_generator a x : generator <[a]> x → x \in <[a]>.

-Lemma generator_order a b : generator <[a]> b → #[a] = #[b].
+Lemma generator_order a b : generator <[a]> b → #[a] = #[b].

End Cyclic.
@@ -260,7 +259,7 @@ Euler's theorem
-Theorem Euler_exp_totient a n : coprime a n → a ^ totient n = 1 %[mod n].
+Theorem Euler_exp_totient a n : coprime a n → a ^ totient n = 1 %[mod n].

Section Eltm.
@@ -269,29 +268,29 @@ Variables (aT rT : finGroupType) (x : aT) (y : rT).

-Definition eltm of #[y] %| #[x] := fun x_i ⇒ y ^+ invm (injm_Zpm x) x_i.
+Definition eltm of #[y] %| #[x] := fun x_i ⇒ y ^+ invm (injm_Zpm x) x_i.

-Hypothesis dvd_y_x : #[y] %| #[x].
+Hypothesis dvd_y_x : #[y] %| #[x].

-Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i.
+Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i.

-Lemma eltm_id : eltm dvd_y_x x = y.
+Lemma eltm_id : eltm dvd_y_x x = y.

-Lemma eltmM : {in <[x]> &, {morph eltm dvd_y_x : x_i x_j / x_i × x_j}}.
+Lemma eltmM : {in <[x]> &, {morph eltm dvd_y_x : x_i x_j / x_i × x_j}}.
Canonical eltm_morphism := Morphism eltmM.

-Lemma im_eltm : eltm dvd_y_x @* <[x]> = <[y]>.
+Lemma im_eltm : eltm dvd_y_x @* <[x]> = <[y]>.

-Lemma ker_eltm : 'ker (eltm dvd_y_x) = <[x ^+ #[y]]>.
+Lemma ker_eltm : 'ker (eltm dvd_y_x) = <[x ^+ #[y]]>.

-Lemma injm_eltm : 'injm (eltm dvd_y_x) = (#[x] %| #[y]).
+Lemma injm_eltm : 'injm (eltm dvd_y_x) = (#[x] %| #[y]).

End Eltm.
@@ -310,12 +309,12 @@
Lemma cycle_sub_group (a : gT) m :
-     m %| #[a] →
-  [set H : {group gT} | H \subset <[a]> & #|H| == m]
-     = [set <[a ^+ (#[a] %/ m)]>%G].
+     m %| #[a] →
+  [set H : {group gT} | H \subset <[a]> & #|H| == m]
+     = [set <[a ^+ (#[a] %/ m)]>%G].

-Lemma cycle_subgroup_char a (H : {group gT}) : H \subset <[a]> → H \char <[a]>.
+Lemma cycle_subgroup_char a (H : {group gT}) : H \subset <[a]> → H \char <[a]>.

End CycleSubGroup.
@@ -333,14 +332,14 @@
Variables aT rT : finGroupType.
-Variables (D : {group aT}) (f : {morphism D >-> rT}) (x : aT).
-Hypothesis Dx : x \in D.
+Variables (D : {group aT}) (f : {morphism D >-> rT}) (x : aT).
+Hypothesis Dx : x \in D.

-Lemma morph_order : #[f x] %| #[x].
+Lemma morph_order : #[f x] %| #[x].

-Lemma morph_generator A : generator A x → generator (f @* A) (f x).
+Lemma morph_generator A : generator A x → generator (f @* A) (f x).

End MorphicImage.
@@ -350,47 +349,47 @@
Variables gT : finGroupType.
-Implicit Types (aT rT : finGroupType) (G H K : {group gT}).
+Implicit Types (aT rT : finGroupType) (G H K : {group gT}).

-Lemma cyclicS G H : H \subset G → cyclic G → cyclic H.
+Lemma cyclicS G H : H \subset G → cyclic G → cyclic H.

-Lemma cyclicJ G x : cyclic (G :^ x) = cyclic G.
+Lemma cyclicJ G x : cyclic (G :^ x) = cyclic G.

Lemma eq_subG_cyclic G H K :
-  cyclic G → H \subset G → K \subset G → (H :==: K) = (#|H| == #|K|).
+  cyclic G → H \subset G → K \subset G → (H :==: K) = (#|H| == #|K|).

Lemma cardSg_cyclic G H K :
-  cyclic G → H \subset G → K \subset G → (#|H| %| #|K|) = (H \subset K).
+  cyclic G → H \subset G → K \subset G → (#|H| %| #|K|) = (H \subset K).

-Lemma sub_cyclic_char G H : cyclic G → (H \char G) = (H \subset G).
+Lemma sub_cyclic_char G H : cyclic G → (H \char G) = (H \subset G).

-Lemma morphim_cyclic rT G H (f : {morphism G >-> rT}) :
-  cyclic H → cyclic (f @* H).
+Lemma morphim_cyclic rT G H (f : {morphism G >-> rT}) :
+  cyclic H → cyclic (f @* H).

-Lemma quotient_cycle x H : x \in 'N(H) → <[x]> / H = <[coset H x]>.
+Lemma quotient_cycle x H : x \in 'N(H) → <[x]> / H = <[coset H x]>.

-Lemma quotient_cyclic G H : cyclic G → cyclic (G / H).
+Lemma quotient_cyclic G H : cyclic G → cyclic (G / H).

Lemma quotient_generator x G H :
-  x \in 'N(H) → generator G x → generator (G / H) (coset H x).
+  x \in 'N(H) → generator G x → generator (G / H) (coset H x).

-Lemma prime_cyclic G : prime #|G| → cyclic G.
+Lemma prime_cyclic G : prime #|G| → cyclic G.

-Lemma dvdn_prime_cyclic G p : prime p → #|G| %| p → cyclic G.
+Lemma dvdn_prime_cyclic G p : prime p → #|G| %| p → cyclic G.

-Lemma cyclic_small G : #|G| ≤ 3 → cyclic G.
+Lemma cyclic_small G : #|G| ≤ 3 → cyclic G.

End CyclicProps.
@@ -400,22 +399,22 @@
Variables gT rT : finGroupType.
-Implicit Types (G H : {group gT}) (M : {group rT}).
+Implicit Types (G H : {group gT}) (M : {group rT}).

-Lemma injm_cyclic G H (f : {morphism G >-> rT}) :
-  'injm f → H \subset G → cyclic (f @* H) = cyclic H.
+Lemma injm_cyclic G H (f : {morphism G >-> rT}) :
+  'injm f → H \subset G → cyclic (f @* H) = cyclic H.

-Lemma isog_cyclic G M : G \isog M → cyclic G = cyclic M.
+Lemma isog_cyclic G M : G \isog M → cyclic G = cyclic M.

-Lemma isog_cyclic_card G M : cyclic G → isog G M = cyclic M && (#|M| == #|G|).
+Lemma isog_cyclic_card G M : cyclic G → isog G M = cyclic M && (#|M| == #|G|).

-Lemma injm_generator G H (f : {morphism G >-> rT}) x :
-    'injm f → x \in G → H \subset G →
-  generator (f @* H) (f x) = generator H x.
+Lemma injm_generator G H (f : {morphism G >-> rT}) x :
+    'injm f → x \in G → H \subset G →
+  generator (f @* H) (f x) = generator H x.

End IsoCyclic.
@@ -431,25 +430,25 @@
Variable gT : finGroupType.
-Implicit Types (A : {set gT}) (G H : {group gT}).
+Implicit Types (A : {set gT}) (G H : {group gT}).

Definition metacyclic A :=
-  [∃ H : {group gT}, [&& cyclic H, H <| A & cyclic (A / H)]].
+  [∃ H : {group gT}, [&& cyclic H, H <| A & cyclic (A / H)]].

Lemma metacyclicP A :
-  reflect (∃ H : {group gT}, [/\ cyclic H, H <| A & cyclic (A / H)])
+  reflect (∃ H : {group gT}, [/\ cyclic H, H <| A & cyclic (A / H)])
          (metacyclic A).

Lemma metacyclic1 : metacyclic 1.

-Lemma cyclic_metacyclic A : cyclic A → metacyclic A.
+Lemma cyclic_metacyclic A : cyclic A → metacyclic A.

-Lemma metacyclicS G H : H \subset G → metacyclic G → metacyclic H.
+Lemma metacyclicS G H : H \subset G → metacyclic G → metacyclic H.

End Metacyclic.
@@ -478,13 +477,13 @@ Section CycleMorphism.

-Variable n : nat.
+Variable n : nat.

-Definition cyclem of gT := fun x : gT ⇒ x ^+ n.
+Definition cyclem of gT := fun x : gT ⇒ x ^+ n.

-Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x × y}}.
+Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x × y}}.

Canonical cyclem_morphism := Morphism cyclemM.
@@ -496,13 +495,13 @@ Section ZpUnitMorphism.

-Variable u : {unit 'Z_#[a]}.
+Variable u : {unit 'Z_#[a]}.

-Lemma injm_cyclem : 'injm (cyclem (val u) a).
+Lemma injm_cyclem : 'injm (cyclem (val u) a).

-Lemma im_cyclem : cyclem (val u) a @* <[a]> = <[a]>.
+Lemma im_cyclem : cyclem (val u) a @* <[a]> = <[a]>.

Definition Zp_unitm := aut injm_cyclem im_cyclem.
@@ -511,56 +510,56 @@ End ZpUnitMorphism.

-Lemma Zp_unitmM : {in units_Zp #[a] &, {morph Zp_unitm : u v / u × v}}.
+Lemma Zp_unitmM : {in units_Zp #[a] &, {morph Zp_unitm : u v / u × v}}.

Canonical Zp_unit_morphism := Morphism Zp_unitmM.

-Lemma injm_Zp_unitm : 'injm Zp_unitm.
+Lemma injm_Zp_unitm : 'injm Zp_unitm.

-Lemma generator_coprime m : generator <[a]> (a ^+ m) = coprime #[a] m.
+Lemma generator_coprime m : generator <[a]> (a ^+ m) = coprime #[a] m.

-Lemma im_Zp_unitm : Zp_unitm @* units_Zp #[a] = Aut <[a]>.
+Lemma im_Zp_unitm : Zp_unitm @* units_Zp #[a] = Aut <[a]>.

-Lemma Zp_unit_isom : isom (units_Zp #[a]) (Aut <[a]>) Zp_unitm.
+Lemma Zp_unit_isom : isom (units_Zp #[a]) (Aut <[a]>) Zp_unitm.

-Lemma Zp_unit_isog : isog (units_Zp #[a]) (Aut <[a]>).
+Lemma Zp_unit_isog : isog (units_Zp #[a]) (Aut <[a]>).

-Lemma card_Aut_cycle : #|Aut <[a]>| = totient #[a].
+Lemma card_Aut_cycle : #|Aut <[a]>| = totient #[a].

-Lemma totient_gen : totient #[a] = #|[set x | generator <[a]> x]|.
+Lemma totient_gen : totient #[a] = #|[set x | generator <[a]> x]|.

-Lemma Aut_cycle_abelian : abelian (Aut <[a]>).
+Lemma Aut_cycle_abelian : abelian (Aut <[a]>).

End CycleAutomorphism.

-Variable G : {group gT}.
+Variable G : {group gT}.

-Lemma Aut_cyclic_abelian : cyclic G → abelian (Aut G).
+Lemma Aut_cyclic_abelian : cyclic G → abelian (Aut G).

-Lemma card_Aut_cyclic : cyclic G → #|Aut G| = totient #|G|.
+Lemma card_Aut_cyclic : cyclic G → #|Aut G| = totient #|G|.

Lemma sum_ncycle_totient :
-  \sum_(d < #|G|.+1) #|[set <[x]> | x in G & #[x] == d]| × totient d = #|G|.
+  \sum_(d < #|G|.+1) #|[set <[x]> | x in G & #[x] == d]| × totient d = #|G|.

End CyclicAutomorphism.

-Lemma sum_totient_dvd n : \sum_(d < n.+1 | d %| n) totient d = n.
+Lemma sum_totient_dvd n : \sum_(d < n.+1 | d %| n) totient d = n.

Section FieldMulCyclic.
@@ -577,29 +576,29 @@ Import GRing.Theory.

-Variables (gT : finGroupType) (G : {group gT}).
+Variables (gT : finGroupType) (G : {group gT}).

Lemma order_inj_cyclic :
-  {in G &, ∀ x y, #[x] = #[y] → <[x]> = <[y]>} → cyclic G.
+  {in G &, ∀ x y, #[x] = #[y] → <[x]> = <[y]>} → cyclic G.

-Lemma div_ring_mul_group_cyclic (R : unitRingType) (f : gT → R) :
-    f 1 = 1%R → {in G &, {morph f : u v / u × v >-> (u × v)%R}} →
-    {in G^#, ∀ x, f x - 1 \in GRing.unit}%R →
-  abelian G → cyclic G.
+Lemma div_ring_mul_group_cyclic (R : unitRingType) (f : gT → R) :
+    f 1 = 1%R → {in G &, {morph f : u v / u × v >-> (u × v)%R}} →
+    {in G^#, ∀ x, f x - 1 \in GRing.unit}%R →
+  abelian G → cyclic G.

-Lemma field_mul_group_cyclic (F : fieldType) (f : gT → F) :
-    {in G &, {morph f : u v / u × v >-> (u × v)%R}} →
-    {in G, ∀ x, f x = 1%R ↔ x = 1} →
+Lemma field_mul_group_cyclic (F : fieldType) (f : gT → F) :
+    {in G &, {morph f : u v / u × v >-> (u × v)%R}} →
+    {in G, ∀ x, f x = 1%R ↔ x = 1} →
  cyclic G.

End FieldMulCyclic.

-Lemma field_unit_group_cyclic (F : finFieldType) (G : {group {unit F}}) :
+Lemma field_unit_group_cyclic (F : finFieldType) (G : {group {unit F}}) :
  cyclic G.

@@ -610,9 +609,9 @@ Import GRing.Theory.

-Lemma has_prim_root (F : fieldType) (n : nat) (rs : seq F) :
-    n > 0 → all n.-unity_root rs → uniq rs → size rs ≥ n →
-  has n.-primitive_root rs.
+Lemma has_prim_root (F : fieldType) (n : nat) (rs : seq F) :
+    n > 0 → all n.-unity_root rs → uniq rs → size rs ≥ n →
+  has n.-primitive_root rs.

End PrimitiveRoots.
@@ -632,10 +631,10 @@ Variable gT : finGroupType.

-Lemma Aut_prime_cycle_cyclic (a : gT) : prime #[a] → cyclic (Aut <[a]>).
+Lemma Aut_prime_cycle_cyclic (a : gT) : prime #[a] → cyclic (Aut <[a]>).

-Lemma Aut_prime_cyclic (G : {group gT}) : prime #|G| → cyclic (Aut G).
+Lemma Aut_prime_cyclic (G : {group gT}) : prime #|G| → cyclic (Aut G).

End AutPrime.
-- cgit v1.2.3