Theorem: PolynomialMap.LocFinsupp_zero (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
S : Type u
x✝² : CommRing S
x✝¹ : Algebra R S
x✝ : S ⊗[R] M
⊢ (Function.support fun i => (0 i).toFun' S x✝).Finite
Tactic:
simp only [Pi.zero_apply, zero_def, Function.support_zero, Set.finite_empty]
State after:
no goals