units_eq_one

Mathlib.Algebra.Group.Nat.Units

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

English

For every unit u in ℕˣ, u = 1.

Русский

Для любого юнита u ∈ ℕˣ имеет место u = 1.

LaTeX

$$$ \forall u \in \mathbb{N}^{\times},\ u = 1 $$$

Lean4

theorem units_eq_one (u : ℕˣ) : u = 1 :=
  Units.ext <| Nat.eq_one_of_dvd_one ⟨u.inv, u.val_inv.symm⟩

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

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

Разделы

Аффилиация

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