freeCommRingPemptyEquivInt — Mathlib

English

The free commutative ring on the empty type is isomorphic to the integers ℤ.

Русский

Свободное коммутативное кольцо на пустом типе изоморфно целым ℤ.

LaTeX

$$$FreeCommRing(\\mathrm{PEmpty}) \\cong_* \\mathbb{Z}$$$

Lean4

/-- The free commutative ring on the empty type is isomorphic to `ℤ`. -/
def freeCommRingPemptyEquivInt : FreeCommRing PEmpty.{u + 1} ≃+* ℤ :=
  RingEquiv.trans (freeCommRingEquivMvPolynomialInt _) (MvPolynomial.isEmptyRingEquiv _ PEmpty)

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