irreducible_iff_prime

Mathlib.Data.Nat.Prime.Defs

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

English

In natural numbers, irreducible elements are precisely primes.

Русский

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

LaTeX

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

Lean4

theorem irreducible_iff_prime {p : ℕ} : Irreducible p ↔ _root_.Prime p :=
  prime_iff

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

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

Разделы

Аффилиация

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