isUnit_iff_abs_eq

Mathlib.Data.Int.Order.Units

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

English

An integer x is a unit in ℤ if and only if |x| = 1.

Русский

Целое число x является единицей в ℤ тогда и только тогда, когда |x| = 1.

LaTeX

$$$\forall x \in \mathbb{Z}, \ \mathrm{IsUnit}(x) \iff |x| = 1.$$$

Lean4

theorem isUnit_iff_abs_eq {x : ℤ} : IsUnit x ↔ abs x = 1 := by
  rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, natCast_inj]

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

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

Разделы

Аффилиация

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