case inl
G : Type ?u.155974
M✝ : Type ?u.155977
N : Type ?u.155980
α : Sort ?u.155983
β : Sort ?u.155986
ι : Sort u_3
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → M
⊢ (0 • ∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), 0 • f i

case inr
G : Type ?u.155974
M✝ : Type ?u.155977
N : Type ?u.155980
α : Sort ?u.155983
β : Sort ?u.155986
ι : Sort u_3
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
f : ι → M
hc : c ≠ 0
⊢ (c • ∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i
G : Type ?u.155974
M✝ : Type ?u.155977
N : Type ?u.155980
α : Sort ?u.155983
β : Sort ?u.155986
ι : Sort u_3
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
f : ι → M
⊢ (c • ∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i
rcases eq_or_ne c 0 with (rfl | hc)
no goals
case inr
G : Type ?u.155974
M✝ : Type ?u.155977
N : Type ?u.155980
α : Sort ?u.155983
β : Sort ?u.155986
ι : Sort u_3
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : R
f : ι → M
hc : c ≠ 0
⊢ (c • ∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), c • f i
exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _
no goals
case inl
G : Type ?u.155974
M✝ : Type ?u.155977
N : Type ?u.155980
α : Sort ?u.155983
β : Sort ?u.155986
ι : Sort u_3
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → M
⊢ (0 • ∑ᶠ (i : ι), f i) = ∑ᶠ (i : ι), 0 • f i
simp