instAddCommMonoidWithOne

Mathlib.Algebra.Ring.Nat

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

English

The natural numbers with addition form a commutative additive monoid with unit 1.

Русский

Числа Натуральные с операцией сложения образуют коммутативный аддитивный моноид с единицей.

LaTeX

$$$(\mathbb{N}, +, 0, 1)$ is a AddCommMonoidWithOne$$

Lean4

instance instAddCommMonoidWithOne : AddCommMonoidWithOne ℕ
    where
  __ := instAddMonoidWithOne
  __ := instAddCommMonoid

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

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

Разделы

Аффилиация

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