English
There is a canonical algebra isomorphism between the polynomial ring in ι indeterminates and the subalgebra of A generated by range x, provided x is algebraically independent.
Русский
Существует каноническое алгебраическое изоморфизм между полиномами в ι переменных и подалгеброй A, сгенерированной порождающими range x, при условии алгебраической независимости x.
LaTeX
$$$\\mathrm{MvPolynomial}_{ι} R \\cong_A R\\; \\text{пс} \\; \\mathrm{algebra\\_indep}_{R}(x) \\Rightarrow \\mathrm{adjoin}(R,\\mathrm{range}\,x)$$$
Lean4
/-- Canonical isomorphism between polynomials and the subalgebra generated by
algebraically independent elements. -/
@[simps! apply_coe]
def aevalEquiv : MvPolynomial ι R ≃ₐ[R] Algebra.adjoin R (range x) :=
(AlgEquiv.ofInjective (aeval x) (algebraicIndependent_iff_injective_aeval.1 hx)).trans
(Subalgebra.equivOfEq _ _ (Algebra.adjoin_range_eq_range_aeval R x).symm)
