isUnit_iff_natAbs_eq

Mathlib.Algebra.Group.Int.Units

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

English

A unit in ℤ is equivalent to its natAbs being equal to 1.

Русский

Единица в ℤ эквивалентна тому, что natAbs(u) = 1.

LaTeX

$$$ IsUnit(u) \iff u\natAbs = 1$$$

Lean4

theorem isUnit_iff_natAbs_eq : IsUnit u ↔ u.natAbs = 1 := by simp [natAbs_eq_iff, isUnit_iff]

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

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

Разделы

Аффилиация

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