subsingleton_ringHom — Mathlib

English

For any ℤ →+* R, there is at most one ring hom ℤ →+* R; indeed these form a singleton.

Русский

Для любого ℤ →+* R существует не более одного кольцевого гомоморфизма ℤ →+* R; это множество синглтон.

LaTeX

$$$\\text{Subsingleton }(\\mathbb{Z} \\to_+* R)$$$

Lean4

instance subsingleton_ringHom {R : Type*} [NonAssocSemiring R] : Subsingleton (ℤ →+* R) :=
  ⟨RingHom.ext_int⟩

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