Library mathcomp.solvable.cyclic
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ Properties of cyclic groups.
+ Definitions:
+ Defined in fingroup.v:
+ < [x]> == the cycle (cyclic group) generated by x.
+ # [x] == the order of x, i.e., the cardinal of < [x]>.
+ Defined in prime.v:
+ totient n == Euler's totient function
+ Definitions in this file:
+ cyclic G <=> G is a cyclic group.
+ metacyclic G <=> G is a metacyclic group (i.e., a cyclic extension of a
+ cyclic group).
+ generator G x <=> x is a generator of the (cyclic) group G.
+ Zpm x == the isomorphism mapping the additive group of integers
+ mod # [x] to the cyclic group < [x]>.
+ cyclem x n == the endomorphism y |-> y ^+ n of < [x]>.
+ Zp_unitm x == the isomorphism mapping the multiplicative group of the
+ units of the ring of integers mod # [x] to the group of
+ automorphisms of < [x]> (i.e., Aut < [x]>).
+ Zp_unitm x maps u to cyclem x u.
+ eltm dvd_y_x == the smallest morphism (with domain < [x]>) mapping x to
+ y, given a proof dvd_y_x : # [y] %| # [x].
+ expg_invn G k == if coprime #|G| k, the inverse of exponent k in G.
+ Basic results for these notions, plus the classical result that any finite
+ group isomorphic to a subgroup of a field is cyclic, hence that Aut G is
+ cyclic when G is of prime order.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GroupScope GRing.Theory.
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GroupScope GRing.Theory.
+ +
+
+ Cyclic groups.
+
+
+
+
+Section Cyclic.
+ +
+Variable gT : finGroupType.
+Implicit Types (a x y : gT) (A B : {set gT}) (G K H : {group gT}).
+ +
+Definition cyclic A := [∃ x, A == <[x]>].
+ +
+Lemma cyclicP A : reflect (∃ x, A = <[x]>) (cyclic A).
+ +
+Lemma cycle_cyclic x : cyclic <[x]>.
+ +
+Lemma cyclic1 : cyclic [1 gT].
+ +
+
+
++Section Cyclic.
+ +
+Variable gT : finGroupType.
+Implicit Types (a x y : gT) (A B : {set gT}) (G K H : {group gT}).
+ +
+Definition cyclic A := [∃ x, A == <[x]>].
+ +
+Lemma cyclicP A : reflect (∃ x, A = <[x]>) (cyclic A).
+ +
+Lemma cycle_cyclic x : cyclic <[x]>.
+ +
+Lemma cyclic1 : cyclic [1 gT].
+ +
+
+ Isomorphism with the additive group
+
+
+
+
+Section Zpm.
+ +
+Variable a : gT.
+ +
+Definition Zpm (i : 'Z_#[a]) := a ^+ i.
+ +
+Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x × y}}.
+ +
+Canonical Zpm_morphism := Morphism ZpmM.
+ +
+Lemma im_Zpm : Zpm @* Zp #[a] = <[a]>.
+ +
+Lemma injm_Zpm : 'injm Zpm.
+ +
+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_isog : isog (Zp #[a]) <[a]>.
+ +
+End Zpm.
+ +
+
+
++Section Zpm.
+ +
+Variable a : gT.
+ +
+Definition Zpm (i : 'Z_#[a]) := a ^+ i.
+ +
+Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x × y}}.
+ +
+Canonical Zpm_morphism := Morphism ZpmM.
+ +
+Lemma im_Zpm : Zpm @* Zp #[a] = <[a]>.
+ +
+Lemma injm_Zpm : 'injm Zpm.
+ +
+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_isog : isog (Zp #[a]) <[a]>.
+ +
+End Zpm.
+ +
+
+ Central and direct product of cycles
+
+
+
+
+Lemma cyclic_abelian A : cyclic A → abelian A.
+ +
+Lemma cycleMsub 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]>.
+ +
+Lemma cyclicM 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).
+ +
+
+
++Lemma cyclic_abelian A : cyclic A → abelian A.
+ +
+Lemma cycleMsub 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]>.
+ +
+Lemma cyclicM 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).
+ +
+
+ Order properties
+
+
+
+
+Lemma order_dvdn a n : #[a] %| n = (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 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_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_prime_order p x : prime p → x ^+ p = 1 → x != 1 → #[x] = p.
+ +
+Lemma orderXdvd a n : #[a ^+ n] %| #[a].
+ +
+Lemma orderXgcd a n : #[a ^+ n] = #[a] %/ gcdn #[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 orderXpfactor p k n x :
+ #[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.
+ +
+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.
+ +
+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))}.
+ +
+Lemma cyclic_dprod K H G :
+ K \x H = G → cyclic K → cyclic H → cyclic G = coprime #|K| #|H| .
+ +
+
+
++Lemma order_dvdn a n : #[a] %| n = (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 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_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_prime_order p x : prime p → x ^+ p = 1 → x != 1 → #[x] = p.
+ +
+Lemma orderXdvd a n : #[a ^+ n] %| #[a].
+ +
+Lemma orderXgcd a n : #[a ^+ n] = #[a] %/ gcdn #[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 orderXpfactor p k n x :
+ #[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.
+ +
+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.
+ +
+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))}.
+ +
+Lemma cyclic_dprod K H G :
+ K \x H = G → cyclic K → cyclic H → cyclic G = coprime #|K| #|H| .
+ +
+
+ Generator
+
+
+
+
+Definition generator (A : {set gT}) a := A == <[a]>.
+ +
+Lemma generator_cycle a : generator <[a]> a.
+ +
+Lemma cycle_generator a x : generator <[a]> x → x \in <[a]>.
+ +
+Lemma generator_order a b : generator <[a]> b → #[a] = #[b].
+ +
+End Cyclic.
+ +
+ +
+
+
++Definition generator (A : {set gT}) a := A == <[a]>.
+ +
+Lemma generator_cycle a : generator <[a]> a.
+ +
+Lemma cycle_generator a x : generator <[a]> x → x \in <[a]>.
+ +
+Lemma generator_order a b : generator <[a]> b → #[a] = #[b].
+ +
+End Cyclic.
+ +
+ +
+
+ Euler's theorem
+
+
+Theorem Euler_exp_totient a n : coprime a n → a ^ totient n = 1 %[mod n].
+ +
+Section Eltm.
+ +
+Variables (aT rT : finGroupType) (x : aT) (y : rT).
+ +
+Definition eltm of #[y] %| #[x] := fun x_i ⇒ y ^+ invm (injm_Zpm x) x_i.
+ +
+Hypothesis dvd_y_x : #[y] %| #[x].
+ +
+Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i.
+ +
+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}}.
+Canonical eltm_morphism := Morphism eltmM.
+ +
+Lemma im_eltm : 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]).
+ +
+End Eltm.
+ +
+Section CycleSubGroup.
+ +
+Variable gT : finGroupType.
+ +
+
+
++ +
+Section Eltm.
+ +
+Variables (aT rT : finGroupType) (x : aT) (y : rT).
+ +
+Definition eltm of #[y] %| #[x] := fun x_i ⇒ y ^+ invm (injm_Zpm x) x_i.
+ +
+Hypothesis dvd_y_x : #[y] %| #[x].
+ +
+Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i.
+ +
+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}}.
+Canonical eltm_morphism := Morphism eltmM.
+ +
+Lemma im_eltm : 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]).
+ +
+End Eltm.
+ +
+Section CycleSubGroup.
+ +
+Variable gT : finGroupType.
+ +
+
+ Gorenstein, 1.3.1 (i)
+
+
+Lemma cycle_sub_group (a : gT) m :
+ 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]>.
+ +
+End CycleSubGroup.
+ +
+
+
++ 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]>.
+ +
+End CycleSubGroup.
+ +
+
+ Reflected boolean property and morphic image, injection, bijection
+
+
+
+
+Section MorphicImage.
+ +
+Variables aT rT : finGroupType.
+Variables (D : {group aT}) (f : {morphism D >-> rT}) (x : aT).
+Hypothesis Dx : x \in D.
+ +
+Lemma morph_order : #[f x] %| #[x].
+ +
+Lemma morph_generator A : generator A x → generator (f @* A) (f x).
+ +
+End MorphicImage.
+ +
+Section CyclicProps.
+ +
+Variables gT : finGroupType.
+Implicit Types (aT rT : finGroupType) (G H K : {group gT}).
+ +
+Lemma cyclicS G H : H \subset G → cyclic G → cyclic H.
+ +
+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|).
+ +
+Lemma cardSg_cyclic G H 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 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_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).
+ +
+Lemma prime_cyclic G : prime #|G| → cyclic G.
+ +
+Lemma dvdn_prime_cyclic G p : prime p → #|G| %| p → cyclic G.
+ +
+Lemma cyclic_small G : #|G| ≤ 3 → cyclic G.
+ +
+End CyclicProps.
+ +
+Section IsoCyclic.
+ +
+Variables gT rT : finGroupType.
+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 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 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.
+ +
+
+
++Section MorphicImage.
+ +
+Variables aT rT : finGroupType.
+Variables (D : {group aT}) (f : {morphism D >-> rT}) (x : aT).
+Hypothesis Dx : x \in D.
+ +
+Lemma morph_order : #[f x] %| #[x].
+ +
+Lemma morph_generator A : generator A x → generator (f @* A) (f x).
+ +
+End MorphicImage.
+ +
+Section CyclicProps.
+ +
+Variables gT : finGroupType.
+Implicit Types (aT rT : finGroupType) (G H K : {group gT}).
+ +
+Lemma cyclicS G H : H \subset G → cyclic G → cyclic H.
+ +
+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|).
+ +
+Lemma cardSg_cyclic G H 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 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_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).
+ +
+Lemma prime_cyclic G : prime #|G| → cyclic G.
+ +
+Lemma dvdn_prime_cyclic G p : prime p → #|G| %| p → cyclic G.
+ +
+Lemma cyclic_small G : #|G| ≤ 3 → cyclic G.
+ +
+End CyclicProps.
+ +
+Section IsoCyclic.
+ +
+Variables gT rT : finGroupType.
+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 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 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.
+ +
+
+ Metacyclic groups.
+
+
+Section Metacyclic.
+ +
+Variable gT : finGroupType.
+Implicit Types (A : {set gT}) (G H : {group gT}).
+ +
+Definition metacyclic A :=
+ [∃ H : {group gT}, [&& cyclic H, H <| A & cyclic (A / H)]].
+ +
+Lemma metacyclicP A :
+ 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 metacyclicS G H : H \subset G → metacyclic G → metacyclic H.
+ +
+End Metacyclic.
+ +
+ +
+
+
++ +
+Variable gT : finGroupType.
+Implicit Types (A : {set gT}) (G H : {group gT}).
+ +
+Definition metacyclic A :=
+ [∃ H : {group gT}, [&& cyclic H, H <| A & cyclic (A / H)]].
+ +
+Lemma metacyclicP A :
+ 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 metacyclicS G H : H \subset G → metacyclic G → metacyclic H.
+ +
+End Metacyclic.
+ +
+ +
+
+ Automorphisms of cyclic groups.
+
+
+Section CyclicAutomorphism.
+ +
+Variable gT : finGroupType.
+ +
+Section CycleAutomorphism.
+ +
+Variable a : gT.
+ +
+Section CycleMorphism.
+ +
+Variable n : nat.
+ +
+Definition cyclem of gT := fun x : gT ⇒ x ^+ n.
+ +
+Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x × y}}.
+ +
+Canonical cyclem_morphism := Morphism cyclemM.
+ +
+End CycleMorphism.
+ +
+Section ZpUnitMorphism.
+ +
+Variable u : {unit 'Z_#[a]}.
+ +
+Lemma injm_cyclem : 'injm (cyclem (val u) a).
+ +
+Lemma im_cyclem : cyclem (val u) a @* <[a]> = <[a]>.
+ +
+Definition Zp_unitm := aut injm_cyclem im_cyclem.
+ +
+End ZpUnitMorphism.
+ +
+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 generator_coprime m : generator <[a]> (a ^+ m) = coprime #[a] m.
+ +
+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_isog : isog (units_Zp #[a]) (Aut <[a]>).
+ +
+Lemma card_Aut_cycle : #|Aut <[a]>| = totient #[a].
+ +
+Lemma totient_gen : totient #[a] = #|[set x | generator <[a]> x]|.
+ +
+Lemma Aut_cycle_abelian : abelian (Aut <[a]>).
+ +
+End CycleAutomorphism.
+ +
+Variable G : {group gT}.
+ +
+Lemma Aut_cyclic_abelian : cyclic G → abelian (Aut 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|.
+ +
+End CyclicAutomorphism.
+ +
+Lemma sum_totient_dvd n : \sum_(d < n.+1 | d %| n) totient d = n.
+ +
+Section FieldMulCyclic.
+ +
+
+
++ +
+Variable gT : finGroupType.
+ +
+Section CycleAutomorphism.
+ +
+Variable a : gT.
+ +
+Section CycleMorphism.
+ +
+Variable n : nat.
+ +
+Definition cyclem of gT := fun x : gT ⇒ x ^+ n.
+ +
+Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x × y}}.
+ +
+Canonical cyclem_morphism := Morphism cyclemM.
+ +
+End CycleMorphism.
+ +
+Section ZpUnitMorphism.
+ +
+Variable u : {unit 'Z_#[a]}.
+ +
+Lemma injm_cyclem : 'injm (cyclem (val u) a).
+ +
+Lemma im_cyclem : cyclem (val u) a @* <[a]> = <[a]>.
+ +
+Definition Zp_unitm := aut injm_cyclem im_cyclem.
+ +
+End ZpUnitMorphism.
+ +
+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 generator_coprime m : generator <[a]> (a ^+ m) = coprime #[a] m.
+ +
+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_isog : isog (units_Zp #[a]) (Aut <[a]>).
+ +
+Lemma card_Aut_cycle : #|Aut <[a]>| = totient #[a].
+ +
+Lemma totient_gen : totient #[a] = #|[set x | generator <[a]> x]|.
+ +
+Lemma Aut_cycle_abelian : abelian (Aut <[a]>).
+ +
+End CycleAutomorphism.
+ +
+Variable G : {group gT}.
+ +
+Lemma Aut_cyclic_abelian : cyclic G → abelian (Aut 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|.
+ +
+End CyclicAutomorphism.
+ +
+Lemma sum_totient_dvd n : \sum_(d < n.+1 | d %| n) totient d = n.
+ +
+Section FieldMulCyclic.
+ +
+
+ A classic application to finite multiplicative subgroups of fields.
+
+
+
+
+Import GRing.Theory.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+Lemma order_inj_cyclic :
+ {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 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}}) :
+ cyclic G.
+ +
+Section PrimitiveRoots.
+ +
+Open Scope ring_scope.
+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.
+ +
+End PrimitiveRoots.
+ +
+
+
++Import GRing.Theory.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+Lemma order_inj_cyclic :
+ {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 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}}) :
+ cyclic G.
+ +
+Section PrimitiveRoots.
+ +
+Open Scope ring_scope.
+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.
+ +
+End PrimitiveRoots.
+ +
+
+ Cycles of prime order
+
+
+