LeanPool.OrderPQ.IsCyclic

theorem IsCyclic.exists_mulEquiv_of_generators_and_card_eq {α : Type u_1} {β : Type u_2} [Group α] [Group β] {x : α} (hx : ∀ (a : α), a ∈ Subgroup.zpowers x) {y : β} (hy : ∀ (b : β), b ∈ Subgroup.zpowers y) (h : Nat.card α = Nat.card β) : ∃ (f : α ≃* β), f x = y

theorem IsAddCyclic.exists_addEquiv_of_generators_and_card_eq {α : Type u_1} {β : Type u_2} [AddGroup α] [AddGroup β] {x : α} (hx : ∀ (a : α), a ∈ AddSubgroup.zmultiples x) {y : β} (hy : ∀ (b : β), b ∈ AddSubgroup.zmultiples y) (h : Nat.card α = Nat.card β) : ∃ (f : α ≃+ β), f x = y

theorem IsCyclic.card_orderOf_dvd_eq {α : Type u_1} [Group α] [IsCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) : {a : α | orderOf a ∣ d}.card = d

theorem IsAddCyclic.card_addOrderOf_dvd_eq {α : Type u_1} [AddGroup α] [IsAddCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) : {a : α | addOrderOf a ∣ d}.card = d

@[implicit_reducible]

def IsCyclic.instCommGroupLeanPool {α : Type u_1} [Group α] [IsCyclic α] : CommGroup α

A cyclic group is a commutative group.

Equations

• IsCyclic.instCommGroupLeanPool = IsCyclic.commGroup

@[implicit_reducible]

def IsAddCyclic.instAddCommGroupLeanPool {α : Type u_1} [AddGroup α] [IsAddCyclic α] : AddCommGroup α

A cyclic additive group is a commutative additive group.

Equations

• IsAddCyclic.instAddCommGroupLeanPool = IsAddCyclic.addCommGroup

theorem IsCyclic.card_torsionBy' {α : Type u_1} [Group α] [IsCyclic α] [Finite α] {d : ℕ} (hd : d ∣ Nat.card α) : Nat.card ↥(Subgroup.torsionBy' α d) = d

theorem IsAddCyclic.card_torsionBy' {α : Type u_1} [AddGroup α] [IsAddCyclic α] [Finite α] {d : ℕ} (hd : d ∣ Nat.card α) : Nat.card ↥(AddSubgroup.torsionBy' α d) = d

theorem IsCyclic.subgroup_eq {α : Type u_1} [Group α] [IsCyclic α] [Finite α] (s : Subgroup α) [Finite ↥s] : s = Subgroup.torsionBy' α (Nat.card ↥s)

theorem IsAddCyclic.addSubgroup_eq {α : Type u_1} [AddGroup α] [IsAddCyclic α] [Finite α] (s : AddSubgroup α) [Finite ↥s] : s = AddSubgroup.torsionBy' α (Nat.card ↥s)

theorem IsCyclic.subgroup_eq_of_card_eq {α : Type u_1} [Group α] [IsCyclic α] [Finite α] (s t : Subgroup α) [Finite ↥s] [Finite ↥t] (h : Nat.card ↥s = Nat.card ↥t) : s = t

theorem IsAddCyclic.addSubgroup_eq_of_card_eq {α : Type u_1} [AddGroup α] [IsAddCyclic α] [Finite α] (s t : AddSubgroup α) [Finite ↥s] [Finite ↥t] (h : Nat.card ↥s = Nat.card ↥t) : s = t

theorem IsCyclic.isCyclic_prod_iff_coprime_card {G1 G2 : Type} [Group G1] [Finite G1] [Group G2] [Finite G2] [IsCyclic G1] [IsCyclic G2] : (Nat.card G1).Coprime (Nat.card G2) ↔ IsCyclic (G1 × G2)

theorem Finite.of_card_eq_neZero {n : ℕ} [NeZero n] {α : Type u_1} (h : Nat.card α = n) : Finite α

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

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

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

noncomputable def MulEquiv.ofPrimeCardEq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} {H : Type u_2} [Group G] [Group H] (hG : Nat.card G = p) (hH : Nat.card H = p) : G ≃* H

Any two groups of the same prime order are isomorphic.

Equations

• MulEquiv.ofPrimeCardEq hG hH = mulEquivOfCyclicCardEq ⋯

noncomputable def AddEquiv.ofPrimeCardEq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (hG : Nat.card G = p) (hH : Nat.card H = p) : G ≃+ H

Any two additive groups of the same prime order are isomorphic.

Equations

• AddEquiv.ofPrimeCardEq hG hH = addEquivOfAddCyclicCardEq ⋯