English
The prime divisors of the characteristic of a finite commutative ring R are exactly the prime divisors of its cardinality.
Русский
Единичные простые делители характеристики конечного коммутативного кольца R совпадают с простыми делителями кардинальности R.
LaTeX
$$$p \mid \operatorname{ringChar}(R) \iff p \mid |R| \quad (R\text{ finite commutative ring}).$$$
Lean4
/-- The prime divisors of the characteristic of a finite commutative ring are exactly
the prime divisors of its cardinality. -/
theorem prime_dvd_char_iff_dvd_card {R : Type*} [CommRing R] [Fintype R] (p : ℕ) [Fact p.Prime] :
p ∣ ringChar R ↔ p ∣ Fintype.card R :=
by
refine
⟨fun h =>
h.trans <|
Int.natCast_dvd_natCast.mp <|
(CharP.intCast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <| mod_cast Nat.cast_card_eq_zero R,
fun h => ?_⟩
by_contra h₀
rcases exists_prime_addOrderOf_dvd_card p h with ⟨r, hr⟩
have hr₁ := addOrderOf_nsmul_eq_zero r
rw [hr, nsmul_eq_mul] at hr₁
rcases IsUnit.exists_left_inv ((isUnit_iff_not_dvd_char R p).mpr h₀) with ⟨u, hu⟩
apply_fun (· * ·) u at hr₁
rw [mul_zero, ← mul_assoc, hu, one_mul] at hr₁
exact mt AddMonoid.addOrderOf_eq_one_iff.mpr (ne_of_eq_of_ne hr (Nat.Prime.ne_one Fact.out)) hr₁
