eq_zero_of_abs_lt_dvd

Mathlib.Algebra.Order.Group.Unbundled.Int

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

← MathLib Explorer

English

If m divides x and |x| < m, then x = 0.

Русский

Если m делится на x и |x| < m, то x = 0.

LaTeX

$$$ (m \mid x) \land |x| < m \Rightarrow x = 0. $$$

Lean4

theorem eq_zero_of_abs_lt_dvd {m x : ℤ} (h1 : m ∣ x) (h2 : |x| < m) : x = 0 :=
  by
  by_contra h
  have := Int.natAbs_le_of_dvd_ne_zero h1 h
  rw [Int.abs_eq_natAbs] at h2
  cutsat

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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