unique_addUnits

Mathlib.Algebra.Group.Nat.Units

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

English

There is a canonical unique element in AddUnits ℕ, namely 0.

Русский

В AddUnits ℕ существует единственный элемент — 0.

LaTeX

$$$ \text{Unique } \mathrm{AddUnits}(\mathbb{N}) $$$

Lean4

instance unique_addUnits : Unique (AddUnits ℕ) where
  default := 0
  uniq := Nat.addUnits_eq_zero

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

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

Разделы

Аффилиация

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