no goals
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Fintype.card α
classical
  rw [orderOf_eq_card_zpowers]
  apply Fintype.card_of_finset'
  simpa using hx
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ Fintype.card { x // x ∈ zpowers g } = Fintype.card α
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Fintype.card α
rw [orderOf_eq_card_zpowers]
case H
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ ∀ (x : α), x ∈ Finset.univ ↔ x ∈ ↑(zpowers g)
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ Fintype.card { x // x ∈ zpowers g } = Fintype.card α
apply Fintype.card_of_finset'
no goals
case H
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ ∀ (x : α), x ∈ Finset.univ ↔ x ∈ ↑(zpowers g)
simpa using hx