char_prime_of_ne_zero

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#CharP.char_prime_of_ne_zero

← MathLib Explorer

English

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

Русский

Если R имеет CharP R p и p ≠ 0, то p является простым.

LaTeX

$$$p \neq 0 \Rightarrow CharP\,R\,p \Rightarrow Nat.Prime\,p$$$

Lean4

/-- The characteristic is prime if it is non-zero. -/
theorem char_prime_of_ne_zero {p : ℕ} [CharP R p] (hp : p ≠ 0) : p.Prime :=
  (CharP.char_is_prime_or_zero R p).resolve_right hp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru