supported_eq_adjoin_X — Mathlib

English

The subalgebra of polynomials supported on s is the algebra generated by the variables X_i for i ∈ s.

Русский

Подалгебра, состоящая из многочленов, поддерживаемых на s, равна той подалгебре, которая порождается переменными X_i для i ∈ s.

LaTeX

$$$$ \mathrm{supported}(R,s) = \mathrm{Algebra.adjoin}_R (X''s) $$$$

Lean4

theorem supported_eq_adjoin_X : supported R s = Algebra.adjoin R (X '' s) :=
  rfl

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