ringChar_of_prime_eq_zero — Mathlib

English

If p is prime and p maps to 0 in R, then the ring characteristic of R is p.

Русский

Если p простое и p ↦ 0 в R, то характеристика кольца R равна p.

LaTeX

$$$ Nat.Prime\ p \rightarrow (p : R) = 0 \rightarrow ringChar\ R = p $$$

Lean4

theorem ringChar_of_prime_eq_zero [Nontrivial R] {p : ℕ} (hprime : Nat.Prime p) (hp0 : (p : R) = 0) : ringChar R = p :=
  Or.resolve_left ((Nat.dvd_prime hprime).1 (ringChar.dvd hp0)) ringChar_ne_one

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