ι : Type ?u.609092
α : Type u_1
β : Type ?u.609098
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
⊢ Fintype.card { x // x ∈ Subgroup.zpowers f } = Fintype.card { x // x ∈ support f }
ι : Type ?u.609092
α : Type u_1
β : Type ?u.609098
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
⊢ orderOf f = card (support f)
rw [orderOf_eq_card_zpowers, ← Fintype.card_coe]
no goals
ι : Type ?u.609092
α : Type u_1
β : Type ?u.609098
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : IsCycle f
⊢ Fintype.card { x // x ∈ Subgroup.zpowers f } = Fintype.card { x // x ∈ support f }
convert Fintype.card_congr (IsCycle.zpowersEquivSupport hf)