support_smul_eq — Mathlib

English

If the scalar b is nonzero, then multiplying a finsupp by b does not change its support when the base is a NoZeroSmulDivisors domain and SMulWithZero holds.

Русский

Если скаляр b не равен нулю, то умножение finsupp на b не меняет поддержку при условии NoZeroSmulDivisors и SMulWithZero.

LaTeX

$$$[Zero R][Zero M][SMulWithZero R M][NoZeroSmulDivisors R M]\\; b \\neq 0 \\Rightarrow (b \\cdot g).\\mathrm{support} = g.\\mathrm{support}$$$

Lean4

@[simp]
theorem support_smul_eq [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {b : R} (hb : b ≠ 0)
    {g : α →₀ M} : (b • g).support = g.support :=
  Finset.ext fun a => by simp [Finsupp.smul_apply, hb]

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