int_algebra_subsingleton — Mathlib

English

There is a unique ℤ-algebra structure on any ring R; i.e., the ℤ-algebra structure is predetermined and unique.

Русский

Для любого кольца R существует единственная структура ℤ-алгебры; то есть структура ℤ-алгебры определена однозначно.

LaTeX

$$$\operatorname{Subsingleton}(\mathrm{Algebra}\ \mathbb{Z}\ R).$$$

Lean4

instance int_algebra_subsingleton : Subsingleton (Algebra ℤ R) :=
  ⟨fun P Q => Algebra.algebra_ext P Q <| RingHom.congr_fun <| Subsingleton.elim _ _⟩

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