natAbs_sub_ne_zero_iff

Mathlib.Algebra.Order.Group.Unbundled.Int

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

English

natAbs(i - j) ≠ 0 iff i ≠ j.

Русский

natAbs(i - j) ≠ 0 тогда и только тогда, когда i ≠ j.

LaTeX

$$$ \operatorname{natAbs}(i - j) \neq 0 \iff i \neq j. $$$

Lean4

theorem natAbs_sub_ne_zero_iff {i j : ℤ} : natAbs (i - j) ≠ 0 ↔ i ≠ j :=
  Nat.ne_zero_iff_zero_lt.trans natAbs_sub_pos_iff

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

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

Разделы

Аффилиация

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