char_is_prime_of_pos

Mathlib.Algebra.CharP.Defs

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

English

If R is a ring with CharP p and NonZero p, then p is a prime: there exists a canonical prime p.

Русский

Если R имеет CharP p и p ненулевой, тогда существует простое p.

LaTeX

$$∀ p, CharP R p → p.Prime$$

Lean4

theorem char_is_prime_of_pos (p : ℕ) [NeZero p] [CharP R p] : Fact p.Prime :=
  ⟨(CharP.char_is_prime_or_zero R _).resolve_right <| NeZero.ne p⟩

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

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

Разделы

Аффилиация

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