unitization — Mathlib

English

There is a natural ℤ-algebra homomorphism from the unitization of a nonunital subring to R.

Русский

Существует каноническое ℤ-алгебра-гомоморфизм от единичизации неединичного подполья в R.

LaTeX

$$$\mathrm{unitization} : \mathrm{Unitization}\;\mathbb{Z}\;s \rightarrow_{\mathbb{Z}} R$$$

Lean4

/-- The natural `ℤ`-algebra homomorphism from the unitization of a non-unital subring to
its `Subring.closure`. -/
def unitization : Unitization ℤ s →ₐ[ℤ] R :=
  NonUnitalSubalgebra.unitization (hSRA := AddSubgroupClass.zsmulMemClass) s

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