charP_of_card_eq_prime_pow — Mathlib

English

If a finite domain R has cardinality p^f for a prime p and f > 0, then CharP R p holds.

Русский

Если конечная области R имеет кардинальность p^f для простого p и f > 0, тогда CharP R p выполняется.

LaTeX

$$$\text{CharP}(R, p) \quad\text{if } |R| = p^f \text{ with } p \text{ prime and } f > 0.$$$

Lean4

theorem charP_of_card_eq_prime_pow {R : Type*} [CommRing R] [IsDomain R] [Fintype R] {p f : ℕ} [hp : Fact p.Prime]
    (hR : Fintype.card R = p ^ f) : CharP R p :=
  have hf : f ≠ 0 := fun h0 ↦ not_subsingleton R <| Fintype.card_le_one_iff_subsingleton.mp <| by simpa [h0] using hR.le
  (CharP.charP_iff_prime_eq_zero hp.out).mpr (by simpa [hf, hR] using Nat.cast_card_eq_zero R)

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