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