emod_lt_abs

Mathlib.Algebra.Order.Group.Unbundled.Int

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

English

If a ∈ Z and b ∈ Z with b ≠ 0, then a mod b < |b|.

Русский

Пусть a,b ∈ Z и b ≠ 0. Тогда a mod b < |b|.

LaTeX

$$$ a \bmod b < |b| \quad \text{если } b \neq 0 $$$

Lean4

theorem emod_lt_abs (a : ℤ) {b : ℤ} (H : b ≠ 0) : a % b < |b| := by rw [← emod_abs];
  exact emod_lt_of_pos _ (abs_pos.2 H)

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

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

Разделы

Аффилиация

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