Documentation

theorem IsCyclic.exists_generator {α : Type u_1} [Group α] [IsCyclic α] :

∃ (g : α), ∀ (x : α), x ∈ Subgroup.zpowers g

theorem IsAddCyclic.exists_generator {α : Type u_1} [AddGroup α] [IsAddCyclic α] :

∃ (g : α), ∀ (x : α), x ∈ AddSubgroup.zmultiples g

theorem isCyclic_iff_exists_zpowers_eq_top {α : Type u_1} [Group α] :

IsCyclic α ↔ ∃ (g : α), Subgroup.zpowers g = ⊤

theorem isAddCyclic_iff_exists_zmultiples_eq_top {α : Type u_1} [AddGroup α] :

IsAddCyclic α ↔ ∃ (g : α), AddSubgroup.zmultiples g = ⊤

theorem Subgroup.isCyclic_iff_exists_zpowers_eq_top {α : Type u_1} [Group α] (H : Subgroup α) :

IsCyclic ↥H ↔ ∃ (g : α), zpowers g = H

theorem AddSubgroup.isAddCyclic_iff_exists_zmultiples_eq_top {α : Type u_1} [AddGroup α] (H : AddSubgroup α) :

IsAddCyclic ↥H ↔ ∃ (g : α), zmultiples g = H

instance Subgroup.isCyclic_zpowers {G : Type u_2} [Group G] (g : G) :

IsCyclic ↥(zpowers g)

instance AddSubgroup.isAddCyclic_zmultiples {G : Type u_2} [AddGroup G] (g : G) :

IsAddCyclic ↥(zmultiples g)

@[instance 100]

instance isCyclic_of_subsingleton {α : Type u_1} [Group α] [Subsingleton α] :

@[instance 100]

instance isAddCyclic_of_subsingleton {α : Type u_1} [AddGroup α] [Subsingleton α] :

@[simp]

theorem isCyclic_multiplicative_iff {α : Type u_1} [SubNegMonoid α] :

IsCyclic (Multiplicative α) ↔ IsAddCyclic α

instance isCyclic_multiplicative {α : Type u_1} [AddGroup α] [IsAddCyclic α] :

IsCyclic (Multiplicative α)

@[simp]

theorem isAddCyclic_additive_iff {α : Type u_1} [DivInvMonoid α] :

IsAddCyclic (Additive α) ↔ IsCyclic α

instance isAddCyclic_additive {α : Type u_1} [Group α] [IsCyclic α] :

IsAddCyclic (Additive α)

instance IsCyclic.commutative {α : Type u_1} [Group α] [IsCyclic α] :

Std.Commutative fun (x1 x2 : α) => x1 * x2

instance IsAddCyclic.commutative {α : Type u_1} [AddGroup α] [IsAddCyclic α] :

Std.Commutative fun (x1 x2 : α) => x1 + x2

@[implicit_reducible]

def IsCyclic.commGroup {α : Type u_1} [hg : Group α] [IsCyclic α] :

CommGroup α

A cyclic group is always commutative. This is not an instance because often we have a better proof of CommGroup.

Equations

IsCyclic.commGroup = { toGroup := hg, mul_comm := ⋯ }

Instances For

@[implicit_reducible]

def IsAddCyclic.addCommGroup {α : Type u_1} [hg : AddGroup α] [IsAddCyclic α] :

AddCommGroup α

A cyclic group is always commutative. This is not an instance because often we have a better proof of AddCommGroup.

Equations

IsAddCyclic.addCommGroup = { toAddGroup := hg, add_comm := ⋯ }

Instances For

instance instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic {G : Type u_2} [Group G] (H : Subgroup G) [IsCyclic ↥H] :

IsMulCommutative ↥H

theorem Nontrivial.of_not_isCyclic {α : Type u_1} [Group α] (nc : ¬IsCyclic α) :

Nontrivial α

A non-cyclic multiplicative group is non-trivial.

theorem Nontrivial.of_not_isAddCyclic {α : Type u_1} [AddGroup α] (nc : ¬IsAddCyclic α) :

Nontrivial α

A non-cyclic additive group is non-trivial.

theorem MonoidHom.map_cyclic {G : Type u_2} [Group G] [h : IsCyclic G] (σ : G →* G) :

∃ (m : ℤ), ∀ (g : G), σ g = g ^ m

theorem AddMonoidHom.map_addCyclic {G : Type u_2} [AddGroup G] [h : IsAddCyclic G] (σ : G →+ G) :

∃ (m : ℤ), ∀ (g : G), σ g = m • g

theorem isCyclic_iff_exists_orderOf_eq_natCard {α : Type u_1} [Group α] [Finite α] :

IsCyclic α ↔ ∃ (g : α), orderOf g = Nat.card α

theorem isAddCyclic_iff_exists_addOrderOf_eq_natCard {α : Type u_1} [AddGroup α] [Finite α] :

IsAddCyclic α ↔ ∃ (g : α), addOrderOf g = Nat.card α

theorem isCyclic_iff_exists_natCard_le_orderOf {α : Type u_1} [Group α] [Finite α] :

IsCyclic α ↔ ∃ (g : α), Nat.card α ≤ orderOf g

theorem isAddCyclic_iff_exists_natCard_le_addOrderOf {α : Type u_1} [AddGroup α] [Finite α] :

IsAddCyclic α ↔ ∃ (g : α), Nat.card α ≤ addOrderOf g

theorem isCyclic_of_orderOf_eq_card {α : Type u_1} [Group α] [Finite α] (x : α) (hx : orderOf x = Nat.card α) :

theorem isAddCyclic_of_addOrderOf_eq_card {α : Type u_1} [AddGroup α] [Finite α] (x : α) (hx : addOrderOf x = Nat.card α) :

theorem isCyclic_of_card_le_orderOf {α : Type u_1} [Group α] [Finite α] (x : α) (hx : Nat.card α ≤ orderOf x) :

theorem isAddCyclic_of_card_le_addOrderOf {α : Type u_1} [AddGroup α] [Finite α] (x : α) (hx : Nat.card α ≤ addOrderOf x) :

theorem Subgroup.eq_bot_or_eq_top_of_prime_card {G : Type u_2} [Group G] (H : Subgroup G) [hp : Fact (Nat.Prime (Nat.card G))] :

H = ⊥ ∨ H = ⊤

theorem AddSubgroup.eq_bot_or_eq_top_of_prime_card {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [hp : Fact (Nat.Prime (Nat.card G))] :

H = ⊥ ∨ H = ⊤

theorem zpowers_eq_top_of_prime_card {G : Type u_2} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) :

Subgroup.zpowers g = ⊤

Any non-identity element of a finite group of prime order generates the group.

theorem zmultiples_eq_top_of_prime_card {G : Type u_2} [AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g ≠ 0) :

AddSubgroup.zmultiples g = ⊤

Any non-identity element of a finite group of prime order generates the group.

theorem mem_zpowers_of_prime_card {G : Type u_2} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) :

g' ∈ Subgroup.zpowers g

theorem mem_zmultiples_of_prime_card {G : Type u_2} [AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 0) :

g' ∈ AddSubgroup.zmultiples g

theorem mem_powers_of_prime_card {G : Type u_2} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) :

g' ∈ Submonoid.powers g

theorem mem_multiples_of_prime_card {G : Type u_2} [AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 0) :

g' ∈ AddSubmonoid.multiples g

theorem powers_eq_top_of_prime_card {G : Type u_2} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) :

Submonoid.powers g = ⊤

theorem multiples_eq_top_of_prime_card {G : Type u_2} [AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g ≠ 0) :

AddSubmonoid.multiples g = ⊤

theorem isCyclic_of_prime_card {α : Type u_1} [Group α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card α = p) :

A finite group of prime order is cyclic.

theorem isAddCyclic_of_prime_card {α : Type u_1} [AddGroup α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card α = p) :

A finite group of prime order is cyclic.

theorem isCyclic_of_card_dvd_prime {α : Type u_1} [Group α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card α ∣ p) :

A finite group of order dividing a prime is cyclic.

theorem isAddCyclic_of_card_dvd_prime {α : Type u_1} [AddGroup α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card α ∣ p) :

A finite group of order dividing a prime is cyclic.

theorem isCyclic_of_surjective {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {F : Type u_4} [hH : IsCyclic G'] [FunLike F G' G] [MonoidHomClass F G' G] (f : F) (hf : Function.Surjective ⇑f) :

IsCyclic G

theorem isAddCyclic_of_surjective {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {F : Type u_4} [hH : IsAddCyclic G'] [FunLike F G' G] [AddMonoidHomClass F G' G] (f : F) (hf : Function.Surjective ⇑f) :

IsAddCyclic G

theorem MulEquiv.isCyclic {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] (e : G ≃* G') :

IsCyclic G ↔ IsCyclic G'

theorem AddEquiv.isAddCyclic {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] (e : G ≃+ G') :

IsAddCyclic G ↔ IsAddCyclic G'

theorem orderOf_eq_card_of_forall_mem_zpowers {α : Type u_1} [Group α] {g : α} (hx : ∀ (x : α), x ∈ Subgroup.zpowers g) :

orderOf g = Nat.card α

theorem addOrderOf_eq_card_of_forall_mem_zmultiples {α : Type u_1} [AddGroup α] {g : α} (hx : ∀ (x : α), x ∈ AddSubgroup.zmultiples g) :

addOrderOf g = Nat.card α

theorem orderOf_eq_card_of_forall_mem_powers {α : Type u_1} [Group α] {g : α} (hx : ∀ (x : α), x ∈ Submonoid.powers g) :

orderOf g = Nat.card α

theorem addOrderOf_eq_card_of_forall_mem_multiples {α : Type u_1} [AddGroup α] {g : α} (hx : ∀ (x : α), x ∈ AddSubmonoid.multiples g) :

addOrderOf g = Nat.card α

theorem orderOf_eq_card_of_zpowers_eq_top {G : Type u_2} [Group G] {g : G} (h : Subgroup.zpowers g = ⊤) :

orderOf g = Nat.card G

theorem addOrderOf_eq_card_of_zmultiples_eq_top {G : Type u_2} [AddGroup G] {g : G} (h : AddSubgroup.zmultiples g = ⊤) :

addOrderOf g = Nat.card G

theorem exists_pow_ne_one_of_isCyclic {G : Type u_2} [Group G] [G_cyclic : IsCyclic G] {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Nat.card G) :

∃ (a : G), a ^ k ≠ 1

theorem exists_nsmul_ne_zero_of_isAddCyclic {G : Type u_2} [AddGroup G] [G_addCyclic : IsAddCyclic G] {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Nat.card G) :

∃ (a : G), k • a ≠ 0

theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers {α : Type u_1} [Group α] [Infinite α] {g : α} (h : ∀ (x : α), x ∈ Subgroup.zpowers g) :

orderOf g = 0

theorem Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples {α : Type u_1} [AddGroup α] [Infinite α] {g : α} (h : ∀ (x : α), x ∈ AddSubgroup.zmultiples g) :

addOrderOf g = 0

instance Bot.isCyclic {α : Type u_1} [Group α] :

IsCyclic ↥⊥

instance Bot.isAddCyclic {α : Type u_1} [AddGroup α] :

IsAddCyclic ↥⊥

instance Subgroup.isCyclic {α : Type u_1} [Group α] [IsCyclic α] (H : Subgroup α) :

IsCyclic ↥H

instance AddSubgroup.isAddCyclic {α : Type u_1} [AddGroup α] [IsAddCyclic α] (H : AddSubgroup α) :

IsAddCyclic ↥H

theorem isCyclic_of_injective {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] [IsCyclic G'] (f : G →* G') (hf : Function.Injective ⇑f) :

IsCyclic G

theorem isAddCyclic_of_injective {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] [IsAddCyclic G'] (f : G →+ G') (hf : Function.Injective ⇑f) :

IsAddCyclic G

theorem Subgroup.isCyclic_of_le {G : Type u_2} [Group G] {H H' : Subgroup G} (h : H ≤ H') [IsCyclic ↥H'] :

IsCyclic ↥H

theorem AddSubgroup.isAddCyclic_of_le {G : Type u_2} [AddGroup G] {H H' : AddSubgroup G} (h : H ≤ H') [IsAddCyclic ↥H'] :

IsAddCyclic ↥H

theorem Subgroup.le_zpowers_iff {G : Type u_2} [Group G] (g : G) (H : Subgroup G) :

H ≤ zpowers g ↔ ∃ (n : ℕ), H = zpowers (g ^ n)

theorem AddSubgroup.le_zmultiples_iff {G : Type u_2} [AddGroup G] (g : G) (H : AddSubgroup G) :

H ≤ zmultiples g ↔ ∃ (n : ℕ), H = zmultiples (n • g)

theorem IsCyclic.card_pow_eq_one_le {α : Type u_1} [Group α] [DecidableEq α] [Fintype α] [IsCyclic α] {n : ℕ} (hn0 : 0 < n) :

{a : α | a ^ n = 1}.card ≤ n

theorem IsAddCyclic.card_nsmul_eq_zero_le {α : Type u_1} [AddGroup α] [DecidableEq α] [Fintype α] [IsAddCyclic α] {n : ℕ} (hn0 : 0 < n) :

{a : α | n • a = 0}.card ≤ n

theorem IsCyclic.exists_monoid_generator {α : Type u_1} [Group α] [Finite α] [IsCyclic α] :

∃ (x : α), ∀ (y : α), y ∈ Submonoid.powers x

theorem IsAddCyclic.exists_addMonoid_generator {α : Type u_1} [AddGroup α] [Finite α] [IsAddCyclic α] :

∃ (x : α), ∀ (y : α), y ∈ AddSubmonoid.multiples x

theorem IsCyclic.exists_ofOrder_eq_natCard {α : Type u_1} [Group α] [h : IsCyclic α] :

∃ (g : α), orderOf g = Nat.card α

theorem IsAddCyclic.exists_ofOrder_eq_natCard {α : Type u_1} [AddGroup α] [h : IsAddCyclic α] :

∃ (g : α), addOrderOf g = Nat.card α

noncomputable def MulDistribMulAction.toMonoidHomZModOfIsCyclic (G : Type u_2) [Group G] (M : Type u_4) [Monoid M] [IsCyclic G] [MulDistribMulAction M G] {n : ℕ} (hn : Nat.card G = n) :

M →* ZMod n

A distributive action of a monoid on a finite cyclic group of order n factors through an action on ZMod n.

Equations

MulDistribMulAction.toMonoidHomZModOfIsCyclic G M hn = { toFun := fun (m : M) => ↑⋯.choose, map_one' := ⋯, map_mul' := ⋯ }

Instances For

theorem MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply {G : Type u_2} [Group G] {M : Type u_4} [Monoid M] [IsCyclic G] [MulDistribMulAction M G] {n : ℕ} (hn : Nat.card G = n) (m : M) (g : G) (k : ℤ) (h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k) :

m • g = g ^ k

theorem IsCyclic.unique_zpow_zmod {α : Type u_1} {a : α} [Group α] [Fintype α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) (x : α) :

∃! n : ZMod (Fintype.card α), x = a ^ n.val

theorem IsAddCyclic.unique_zsmul_zmod {α : Type u_1} {a : α} [AddGroup α] [Fintype α] (ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a) (x : α) :

∃! n : ZMod (Fintype.card α), x = n.val • a

theorem IsCyclic.image_range_orderOf {α : Type u_1} {a : α} [Group α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) :

Finset.image (fun (i : ℕ) => a ^ i) (Finset.range (orderOf a)) = Finset.univ

theorem IsAddCyclic.image_range_addOrderOf {α : Type u_1} {a : α} [AddGroup α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a) :

Finset.image (fun (i : ℕ) => i • a) (Finset.range (addOrderOf a)) = Finset.univ

theorem IsCyclic.image_range_card {α : Type u_1} {a : α} [Group α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) :

Finset.image (fun (i : ℕ) => a ^ i) (Finset.range (Nat.card α)) = Finset.univ

theorem IsAddCyclic.image_range_card {α : Type u_1} {a : α} [AddGroup α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a) :

Finset.image (fun (i : ℕ) => i • a) (Finset.range (Nat.card α)) = Finset.univ

theorem IsCyclic.ext {G : Type u_2} [Group G] [Finite G] [IsCyclic G] {d : ℕ} {a b : ZMod d} (hGcard : Nat.card G = d) (h : ∀ (t : G), t ^ a.val = t ^ b.val) :

a = b