Theorem: Weight.sum_smul (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ Weight.sum (k • w) = k * Weight.sum w
Tactic:
simp only [Weight.sum, Finset.mul_sum]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ ∑ j : Fin (Nat.succ n), (k • w) j = ∑ i : Fin (Nat.succ n), k * w i

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ ∑ j : Fin (Nat.succ n), (k • w) j = ∑ i : Fin (Nat.succ n), k * w i
Tactic:
rfl
State after:
no goals