Theorem: MvPolynomial.DirectSum.coeLinearMap_eq_support_sum (DividedPowers/ForMathlib/WeightedHomogeneous.lean)

State before:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
⊢ (DirectSum.coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun x x_1 => ↑x_1
Tactic:
rw [DirectSum.coeLinearMap_eq_dfinsupp_sum]
State after:
no goals