freeRingPunitEquivPolynomialInt — Mathlib

English

The free ring on a type with one term is isomorphic to the polynomial ring ℤ[X].

Русский

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

LaTeX

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

Lean4

/-- The free ring on a type with one term is isomorphic to `ℤ[X]`. -/
def freeRingPunitEquivPolynomialInt : FreeRing PUnit.{u + 1} ≃+* ℤ[X] :=
  RingEquiv.trans (subsingletonEquivFreeCommRing _) freeCommRingPunitEquivPolynomialInt

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