repr — Mathlib

English

There is a canonical algebra homomorphism from the subalgebra generated by range x to the polynomial ring, giving an algebraic bridge between these objects when x is algebraically independent.

Русский

Существует каноническое алгебраическое гомоморфизм от подалгебры, порождаемой range x, в кольцо многочленов.

LaTeX

$$$\\mathrm{repr} : \\mathrm{adjoin}(R, \\mathrm{range}\\,x) \\to_A \\mathrm{MvPolynomial}_{ι} R$$$

Lean4

/-- The canonical map from the subalgebra generated by an algebraic independent family
  into the polynomial ring. -/
def repr : Algebra.adjoin R (range x) →ₐ[R] MvPolynomial ι R :=
  hx.aevalEquiv.symm

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