mem_support_iff — Mathlib

English

An index is in the support of p iff the corresponding coefficient is nonzero.

Русский

Индекс принадлежит опоре p тогда и только тогда, когда соответствующий коэффициент не равен нулю.

LaTeX

$$$ m \in p.support \\\\Leftrightarrow p.coeff m \neq 0 $$$

Lean4

@[simp]
theorem mem_support_iff {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∈ p.support ↔ p.coeff m ≠ 0 := by simp [support, coeff]

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