not_isUnit_prime_of_dvd_card — Mathlib

English

A prime that divides the cardinality of a finite commutative ring R is not a unit in R.

Русский

Пусть простое p делит кардинальность конечного коммутативного кольца R; тогда p не является единицей в R.

LaTeX

$$$p \mid |R| \Rightarrow \neg \mathrm{IsUnit}(p:\,R).$$$

Lean4

/-- A prime that divides the cardinality of a finite commutative ring `R`
isn't a unit in `R`. -/
theorem not_isUnit_prime_of_dvd_card {R : Type*} [CommRing R] [Fintype R] {p : ℕ} [Fact p.Prime]
    (hp : p ∣ Fintype.card R) : ¬IsUnit (p : R) :=
  mt (isUnit_iff_not_dvd_char R p).mp (Classical.not_not.mpr ((prime_dvd_char_iff_dvd_card p).mpr hp))

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