natAbs_le_of_dvd_ne_zero

Mathlib.Data.Int.Basic

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

English

If m divides n and n ≠ 0, then natAbs(m) ≤ natAbs(n).

Русский

Если m делится на n и n ≠ 0, то |m| ≤ |n|.

LaTeX

$$$\\\\forall m,n \\in \\mathbb{Z},\\\\; m \\mid n \\land n \\neq 0 \\Rightarrow |m| \\le |n|$$$

Lean4

theorem natAbs_le_of_dvd_ne_zero (hmn : m ∣ n) (hn : n ≠ 0) : natAbs m ≤ natAbs n :=
  not_lt.mp (mt (eq_zero_of_dvd_of_natAbs_lt_natAbs hmn) hn)

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

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

Разделы

Аффилиация

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