isPrimal

Mathlib.Algebra.Prime.Defs

URI: https://scilib.ai/kg/mathlib#Prime.isPrimal

← MathLib Explorer

English

A prime p is primal.

Русский

Простая p является прималовой (primal).

LaTeX

$$IsPrimal(p)$$

Lean4

theorem isPrimal : IsPrimal p := fun _a _b dvd ↦
  (hp.dvd_or_dvd dvd).elim (fun h ↦ ⟨p, 1, h, one_dvd _, (mul_one p).symm⟩) fun h ↦
    ⟨1, p, one_dvd _, h, (one_mul p).symm⟩

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

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

Разделы

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

Аффилиация

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