English
If R is a finite ring with cardinality p prime and CharP R p, then ZMod p ≃+* R.
Русский
Если R — конечное кольцо с кардинальностью p, где p простое, и CharP R p, то ZMod p ≃+* R.
LaTeX
$$$ ZMod p \cong+* R $$$
Lean4
/-- The unique ring isomorphism between `ZMod p` and a ring `R` of cardinality a prime `p`.
If you need any property of this isomorphism, first of all use `ringEquivOfPrime_eq_ringEquiv`
below (after `have : CharP R p := ...`) and deduce it by the results about `ZMod.ringEquiv`. -/
noncomputable def ringEquivOfPrime [Fintype R] {p : ℕ} (hp : p.Prime) (hR : Fintype.card R = p) : ZMod p ≃+* R :=
have : Nontrivial R :=
Fintype.one_lt_card_iff_nontrivial.1
(hR ▸ hp.one_lt)
-- The following line exists as `charP_of_card_eq_prime` in
-- `Mathlib/Algebra/CharP/CharAndCard.lean`.
have : CharP R p := (CharP.charP_iff_prime_eq_zero hp).2 (hR ▸ Nat.cast_card_eq_zero R)
ZMod.ringEquiv R hR
