unique_units

Mathlib.Algebra.Group.Nat.Units

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

English

There is a canonical unique unit of ℕˣ, namely 1.

Русский

Существует единственный канонический единичный элемент в ℕˣ — 1.

LaTeX

$$$ \text{Unique } \mathbb{N}^{\times} $$$

Lean4

instance unique_units : Unique ℕˣ where
  default := 1
  uniq := Nat.units_eq_one

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

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

Разделы

Аффилиация

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