mem_supported_vars — Mathlib

English

For every polynomial p, p belongs to the subalgebra generated by the variables that occur in p.

Русский

Для любого многочлена p он принадлежит подалгебре, порождаемой переменными, которые встречаются в p.

LaTeX

$$$$ p \in \mathrm{supported}(R, \uparrow p.\mathrm{vars}) $$$$

Lean4

@[simp]
theorem mem_supported_vars (p : MvPolynomial σ R) : p ∈ supported R (↑p.vars : Set σ) := by rw [mem_supported]

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