ringEquiv — Mathlib

English

There exists a unique ring isomorphism between ZMod n and any ring R of characteristic n and cardinality n.

Русский

Существует единственный кольцевой изоморфизм между ZMod n и кольцом R характеристикой n и кардинальностью n.

LaTeX

$$$ ZMod n \cong+* R $$$

Lean4

/-- The unique ring isomorphism between `ZMod n` and a ring `R`
of characteristic `n` and cardinality `n`. -/
noncomputable def ringEquiv [Fintype R] (h : Fintype.card R = n) : ZMod n ≃+* R :=
  RingEquiv.ofBijective _ (ZMod.castHom_bijective R h)

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