char_is_prime

Mathlib.Algebra.CharP.Lemmas

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

English

For a finite ring R with no zero divisors, if CharP R p holds, then p is prime.

Русский

Для конечного кольца R без нулевых делителей, если CharP R p, то p — простое.

LaTeX

$$Nat.Prime(p)$$

Lean4

theorem char_is_prime (p : ℕ) [CharP R p] : p.Prime :=
  Or.resolve_right (char_is_prime_or_zero R p) (char_ne_zero_of_finite R p)

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

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

Разделы

Аффилиация

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