Theorem: PolynomialMap.lfsum_eq (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type u_3
f : ι → M →ₚ[R] N
hf : LocFinsupp f
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ (lfsum f).toFun' S m = (Finsupp.ofSupportFinite (fun i => (f i).toFun' S m) ⋯).sum fun x m => m
Tactic:
rw [lfsum, dif_pos hf]
State after:
no goals