subsingleton_ringHom — Mathlib

English

For any n and any target ring R with a semiring structure, there is at most one ring homomorphism from ZMod n to R.

Русский

Для любых n и кольца R существует не более одного кольцевого одностороннего гомоморфизма из ZMod n в R.

LaTeX

$$$\text{Subsingleton} \ (\mathbb{Z}/n\mathbb{Z} \to+* R)$$$

Lean4

instance subsingleton_ringHom [Semiring R] : Subsingleton (ZMod n →+* R) :=
  ⟨RingHom.ext_zmod⟩

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