prime_iff

Mathlib.Data.Nat.Prime.Defs

URI: https://scilib.ai/kg/mathlib#Nat.prime_iff

English

In natural numbers, irreducible elements coincide with prime elements.

Русский

В натуральных числах неприводимые и простые элементы совпадают.

LaTeX

$$$\\\\forall p \\\\in \\\\mathbb{N}, \\\\mathrm{Irreducible}(p) \\\\iff \\\\mathrm{Prime}(p)$$$

Lean4

theorem prime_iff {p : ℕ} : p.Prime ↔ _root_.Prime p :=
  ⟨fun h => ⟨h.ne_zero, h.not_isUnit, fun _ _ => h.dvd_mul.mp⟩, Prime.irreducible⟩

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

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

Разделы

Аффилиация

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