mvPolynomialOptionEquivPolynomialAdjoin_X_none

English

The image under an algebraic equivalence preserves independence.

Русский

Образ через алгебраическое эквивалентство сохраняет независимость.

LaTeX

$$$\text{AlgebraicIndependent}_R\;\text{on } x \Rightarrow \text{AlgebraicIndependent}_R\;\text{on } x'$, where x' is the image under the equivalence.$$

Lean4

theorem mvPolynomialOptionEquivPolynomialAdjoin_X_none (hx : AlgebraicIndependent R x) :
    hx.mvPolynomialOptionEquivPolynomialAdjoin (X none) = Polynomial.X := by
  rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim, Polynomial.map_X]

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