natAbs_eq_iff_associated — Mathlib

English

For integers a, b, a.natAbs = b.natAbs iff a and b are associated (differ by a unit).

Русский

Для целых a, b: a.natAbs = b.natAbs тогда и только тогда, когда a и b аффилированы (различаются умножением на единицу).

LaTeX

$$$$ a.natAbs = b.natAbs \\iff\\ Associated\\ a\\ b $$$$

Lean4

theorem natAbs_eq_iff_associated {a b : ℤ} : a.natAbs = b.natAbs ↔ Associated a b :=
  by
  refine Int.natAbs_eq_natAbs_iff.trans ?_
  constructor
  · rintro (rfl | rfl)
    · rfl
    · exact ⟨-1, by simp⟩
  · rintro ⟨u, rfl⟩
    obtain rfl | rfl := Int.units_eq_one_or u
    · exact Or.inl (by simp)
    · exact Or.inr (by simp)

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