freeCommRingPunitEquivPolynomialInt

English

The free commutative ring on a one-point type is isomorphic to the polynomial ring ℤ[X].

Русский

Свободное коммутативное кольцо на типе из одного элемента изоморфно кольцу многочленов ℤ[X].

LaTeX

$$$FreeCommRing(\\mathrm{PUnit}) \\cong_* \\mathbb{Z}[X]$$$

Lean4

/-- The free commutative ring on a type with one term is isomorphic to `ℤ[X]`. -/
def freeCommRingPunitEquivPolynomialInt : FreeCommRing PUnit.{u + 1} ≃+* ℤ[X] :=
  (freeCommRingEquivMvPolynomialInt _).trans (MvPolynomial.pUnitAlgEquiv ℤ).toRingEquiv

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