char_is_prime_or_zero — Mathlib

English

If p ≠ 0 and CharP R p, then p is a prime number.

Русский

Если p ≠ 0 и CharP R p, то p — простое число.

LaTeX

$$$CharP\,R\,p \Rightarrow p \text{ prime} \text{ при } p \neq 0$$$

Lean4

theorem char_is_prime_or_zero (p : ℕ) [hc : CharP R p] : Nat.Prime p ∨ p = 0 :=
  match p, hc with
  | 0, _ => Or.inr rfl
  | 1, hc => absurd (Eq.refl (1 : ℕ)) (@char_ne_one R _ _ (1 : ℕ) hc)
  | m + 2, hc => Or.inl (@char_is_prime_of_two_le R _ _ (m + 2) hc (Nat.le_add_left 2 m))

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