support_smul_eq — Mathlib

English

If a is a nonzero element acting on coefficients, then multiplying by a does not change the set of supports (no-zero divisors required beyond NoZeroSmulDivisors).

Русский

Если a не нуль, и действует на коэффициенты, то умножение на a не меняет множество опор (при этом достаточно условий NoZeroSmulDivisors).

LaTeX

$$$a \\neq 0 \\implies (a \\cdot p).\\text{support} = p.\\text{support}$$$

Lean4

@[simp]
theorem support_smul_eq {S₁ : Type*} [Semiring S₁] [Module S₁ R] [NoZeroSMulDivisors S₁ R] {a : S₁} (h : a ≠ 0)
    (p : MvPolynomial σ R) : (a • p).support = p.support :=
  Finsupp.support_smul_eq h

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