mvPolynomialOptionEquivPolynomialAdjoin_X_some

English

The mvPolynomialOptionEquivPolynomialAdjoin maps X (none) to X, and X (some i) to C(a) for a certain a.

Русский

Применение mvPolynomialOptionEquivPolynomialAdjoin отправляет X none в Polynomial.X, а X (some i) в константу C(a).

LaTeX

$$$\text{mvPolynomialOptionEquivPolynomialAdjoin}\; (X\;\text{none}) = X$ and similar for some i$$

Lean4

theorem mvPolynomialOptionEquivPolynomialAdjoin_X_some (hx : AlgebraicIndependent R x) (i) :
    hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i)) = Polynomial.C (hx.aevalEquiv (X i)) := by
  rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim, Polynomial.map_C,
    RingHom.coe_coe]

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