α : Type u_2
M : Type u_1
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
i : α
r : R
⊢ (∑ x : α, if x = i then r • v x else 0) = r • v i
α : Type u_2
M : Type u_1
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
i : α
r : R
⊢ ↑(↑(Fintype.total R S) v) (Pi.single i r) = r • v i
simp_rw [Fintype.total_apply, Pi.single_apply, ite_smul, zero_smul]
no goals
α : Type u_2
M : Type u_1
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
i : α
r : R
⊢ (∑ x : α, if x = i then r • v x else 0) = r • v i
rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]