Theorem: Equiv.Perm.Basis.Kf_apply (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ g (Kf a e (c, i)) = Kf a e (c, i + 1)
Tactic:
rw [Kf_def, Kf_def, ← Equiv.Perm.mul_apply, ← zpow_one_add, add_comm 1 i]
State after:
no goals