IsSupported — Mathlib

English

IsSupported(x, s) means that every monomial appearing in x uses only variables from s, i.e., x lies in the closure of the subring generated by s.

Русский

IsSupported(x, s) означает, что каждый моном, встречающийся в x, использует только переменные из s; т.е. x принадлежит замыканию подкольца, порожденного s.

LaTeX

$$$ \\operatorname{IsSupported}(x, s) \\;\\equiv\\; x \\in \\operatorname{Subring}.closure(\\mathrm{of}''s) $$$

Lean4

/-- `is_supported x s` means that all monomials showing up in `x` have variables in `s`. -/
def IsSupported (x : FreeCommRing α) (s : Set α) : Prop :=
  x ∈ Subring.closure (of '' s)

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