English
There is a canonical ring isomorphism between the free commutative ring on α and the multivariate polynomial ring with integer coefficients in variables indexed by α.
Русский
Существует каноническое кольцевое изоморфизм между свободным коммутативным кольцом на α и многочленным кольцом со взаимно независимыми переменными, индексационными по α и коэффициентами в целых.
LaTeX
$$$FreeCommRing(\\alpha) \\cong_* MvPolynomial(\\alpha, \\mathbb{Z})$$$
Lean4
/-- The free commutative ring on `α` is isomorphic to the polynomial ring over ℤ with
variables in `α` -/
def freeCommRingEquivMvPolynomialInt : FreeCommRing α ≃+* MvPolynomial α ℤ :=
RingEquiv.ofHomInv (FreeCommRing.lift <| (fun a => MvPolynomial.X a : α → MvPolynomial α ℤ))
(MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of) (by ext; simp) (by ext <;> simp)
