instUniqueUnits

Mathlib.SetTheory.Cardinal.Divisibility

URI: https://scilib.ai/kg/mathlib#Cardinal.instUniqueUnits

English

The unit group of cardinals is a singleton; the only unit is 1.

Русский

Группа единиц кардиналов единична; единственная единица — это 1.

LaTeX

$$$\mathrm{Units}(\mathsf{Cardinal}) = \{1\}$$$

Lean4

instance : Unique Cardinal.{u}ˣ where
  default := 1
  uniq a := Units.val_eq_one.mp <| isUnit_iff.mp a.isUnit

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

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

Разделы

Аффилиация

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