natAbs_of_isUnit

Mathlib.Algebra.Group.Int.Units

URI: https://scilib.ai/kg/mathlib#Int.natAbs_of_isUnit

English

If u is a unit, then natAbs u = 1.

Русский

Если u является единицей, то natAbs u = 1.

LaTeX

$$$ \operatorname{natAbs}(u) = 1 \quad\text{если } IsUnit(u)$$$

Lean4

@[simp]
theorem natAbs_of_isUnit (hu : IsUnit u) : natAbs u = 1 :=
  units_natAbs hu.unit

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

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

Разделы

Аффилиация

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