English
For any g, the support of b • g is the same as the support of g; i.e., scalar multiplication by a nonzero scalar does not change the support.
Русский
Для любого g поддержка b • g совпадает с поддержкой g; т.е. умножение на ненулевой скаляр не изменяет поддержку.
LaTeX
$$$[Zero M][SMulZeroClass R M] \\; {b : R} {g : \\alpha \\to_0 M} : (b \\cdot g).\\mathrm{support} = g.\\mathrm{support}$$$
Lean4
theorem support_smul [Zero M] [SMulZeroClass R M] {b : R} {g : α →₀ M} : (b • g).support ⊆ g.support := fun a =>
by
simp only [smul_apply, mem_support_iff, Ne]
exact mt fun h => h.symm ▸ smul_zero _