charP_of_card_eq_prime — Mathlib

English

For a finite commutative ring R and a prime p, p divides the characteristic of R iff p divides the cardinality of R.

Русский

Для конечного коммутативного кольца R и простого p выполняется p делит характеристику R тогда и только тогда, когда p делит кардинальность R.

LaTeX

$$$p \mid \operatorname{ringChar}(R) \iff p \mid |R|.$$$

Lean4

theorem charP_of_card_eq_prime {R : Type*} [NonAssocRing R] [Fintype R] {p : ℕ} [hp : Fact p.Prime]
    (hR : Fintype.card R = p) : CharP R p :=
  have := Fintype.one_lt_card_iff_nontrivial.1 (hR ▸ hp.1.one_lt)
  (CharP.charP_iff_prime_eq_zero hp.1).2 (hR ▸ Nat.cast_card_eq_zero R)

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