exact Fintype.sum_bijective σ (Equiv.bijective _) _ _ (fun k ↦ rfl)
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ ∑ x : Fin (Nat.succ n), a (σ x) * w (σ x) = ∑ j : Fin (Nat.succ n), a j * w j
no goals