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

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : ℕ
⊢ pair (k • w) a = k * pair w a
Tactic:
simp_rw [pair, smul_apply, mul_left_comm]
State after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), k * (a x * w x) = k * ∑ j : Fin (Nat.succ n), a j * w j

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), k * (a x * w x) = k * ∑ j : Fin (Nat.succ n), a j * w j
Tactic:
exact (Finset.mul_sum Finset.univ (fun i ↦ a i * w i) k).symm
State after:
no goals