instUniqueFactorizationMonoid

Mathlib.RingTheory.UniqueFactorizationDomain.Nat

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

English

The natural numbers form a UniqueFactorizationMonoid (UFM).

Русский

Натуральные числа образуют уникальный факторизационный моноид.

LaTeX

$$$UniqueFactorizationMonoid(\mathbb N)$$$

Lean4

instance instUniqueFactorizationMonoid : UniqueFactorizationMonoid ℕ where
  irreducible_iff_prime := Nat.irreducible_iff_prime

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

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

Разделы

Аффилиация

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