Theorem: LinearMap.map_finsum (DividedPowers/ForMathlib/GradedAlgebra.lean)

State before:
α : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module S N
f : α → M
g : M →ₛₗ[σ] N
hf : (Function.support f).Finite
⊢ g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)
Tactic:
rw [← LinearMap.toAddMonoidHom_coe]
State after:
α : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module S N
f : α → M
g : M →ₛₗ[σ] N
hf : (Function.support f).Finite
⊢ g.toAddMonoidHom (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g.toAddMonoidHom (f i)

State before:
α : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module S N
f : α → M
g : M →ₛₗ[σ] N
hf : (Function.support f).Finite
⊢ g.toAddMonoidHom (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g.toAddMonoidHom (f i)
Tactic:
exact AddMonoidHom.map_finsum _ hf
State after:
no goals