English
In a finite commutative ring R, a prime p divides the ring's characteristic exactly when p divides the ring's cardinality; in particular, if p ∣ |R| then p cannot be a unit in R.
Русский
В конечном коммутативном кольце R простое число p делит характеристику R тогда и только тогда, когда p делит кардинальность кольца; в частности, если p ∣ |R|, то p не является единицей в R.
LaTeX
$$$p \mid \operatorname{ringChar}(R) \iff p \mid |R| \quad (R\text{ finite commutative ring}).$$$
Lean4
/-- A prime `p` is a unit in a finite commutative ring `R`
iff it does not divide the characteristic. -/
theorem isUnit_iff_not_dvd_char (R : Type*) [CommRing R] (p : ℕ) [Fact p.Prime] [Finite R] :
IsUnit (p : R) ↔ ¬p ∣ ringChar R :=
isUnit_iff_not_dvd_char_of_ringChar_ne_zero R p <| CharP.char_ne_zero_of_finite R (ringChar R)
