no goals
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx : orderOf x = Fintype.card α
⊢ IsCyclic α
classical
  use x
  simp_rw [← SetLike.mem_coe, ← Set.eq_univ_iff_forall]
  rw [← Fintype.card_congr (Equiv.Set.univ α), orderOf_eq_card_zpowers] at hx
  exact Set.eq_of_subset_of_card_le (Set.subset_univ _) (ge_of_eq hx)
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx : orderOf x = Fintype.card α
⊢ ∀ (x_1 : α), x_1 ∈ zpowers x
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx : orderOf x = Fintype.card α
⊢ IsCyclic α
use x
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx : orderOf x = Fintype.card α
⊢ ↑(zpowers x) = Set.univ
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx : orderOf x = Fintype.card α
⊢ ∀ (x_1 : α), x_1 ∈ zpowers x
simp_rw [← SetLike.mem_coe, ← Set.eq_univ_iff_forall]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx✝ : orderOf x = Fintype.card ↑Set.univ
hx : Fintype.card { x_1 // x_1 ∈ zpowers x } = Fintype.card ↑Set.univ
⊢ ↑(zpowers x) = Set.univ
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx : orderOf x = Fintype.card α
⊢ ↑(zpowers x) = Set.univ
rw [← Fintype.card_congr (Equiv.Set.univ α), orderOf_eq_card_zpowers] at hx
no goals
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx✝ : orderOf x = Fintype.card ↑Set.univ
hx : Fintype.card { x_1 // x_1 ∈ zpowers x } = Fintype.card ↑Set.univ
⊢ ↑(zpowers x) = Set.univ
exact Set.eq_of_subset_of_card_le (Set.subset_univ _) (ge_of_eq hx)