addUnits_eq_zero

Mathlib.Algebra.Group.Nat.Units

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

English

For every AddUnits ℕ element u, u = 0.

Русский

Для любого элемента u ∈ AddUnits ℕ выполняется u = 0.

LaTeX

$$$ \forall u \in \mathrm{AddUnits}(\mathbb{N}),\ u = 0 $$$

Lean4

theorem addUnits_eq_zero (u : AddUnits ℕ) : u = 0 :=
  AddUnits.ext <| (Nat.eq_zero_of_add_eq_zero u.val_neg).1

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

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

Разделы

Аффилиация

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