case intro
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ exponent α = Fintype.card α
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
⊢ exponent α = Fintype.card α
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ exponent α ∣ Fintype.card α

case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Fintype.card α ∣ exponent α
case intro
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ exponent α = Fintype.card α
apply Nat.dvd_antisymm
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ orderOf g ∣ exponent α
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Fintype.card α ∣ exponent α
rw [← orderOf_eq_card_of_forall_mem_zpowers hg]
no goals
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ orderOf g ∣ exponent α
exact order_dvd_exponent _
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ ∀ (b : α), b ∈ Finset.univ → orderOf b ∣ Fintype.card α
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ exponent α ∣ Fintype.card α
rw [← lcm_order_eq_exponent, Finset.lcm_dvd_iff]
no goals
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ ∀ (b : α), b ∈ Finset.univ → orderOf b ∣ Fintype.card α
exact fun b _ => orderOf_dvd_card_univ