subsingleton_ringEquiv — Mathlib

English

For any n and any R with a semiring structure, there is at most one ring equivalence ZMod n ≃+* R.

Русский

Для любых n и R с полным полем полукольца существует не более одной эквивалентности ZMod n ≃+* R.

LaTeX

$$$\text{Subsingleton} (ZMod\ n \simeq+* R)$$$

Lean4

instance subsingleton_ringEquiv [Semiring R] : Subsingleton (ZMod n ≃+* R) :=
  ⟨fun f g => by
    rw [RingEquiv.coe_ringHom_inj_iff]
    apply RingHom.ext_zmod _ _⟩

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