support_smul — Mathlib

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 _

Похожие утверждения