mabs_div_lt_of_one_le_of_lt — Mathlib

English

1 ≤ a < n and 1 ≤ b < n imply |a/b|_m < n.

Русский

1 ≤ a < n и 1 ≤ b < n предполагают |a/b|_м < n.

LaTeX

$$$1 \le a \land a < n \land 1 \le b \land b < n \implies \left| \frac{a}{b} \right|_m < n$$$

Lean4

/-- `|a / b|ₘ < n` if `1 ≤ a < n` and `1 ≤ b < n`. -/
@[to_additive /-- `|a - b| < n` if `0 ≤ a < n` and `0 ≤ b < n`. -/
    ]
theorem mabs_div_lt_of_one_le_of_lt {a b n : G} (one_le_a : 1 ≤ a) (a_lt_n : a < n) (one_le_b : 1 ≤ b)
    (b_lt_n : b < n) : |a / b|ₘ < n :=
  by
  rw [mabs_div_lt_iff, div_lt_iff_lt_mul, div_lt_iff_lt_mul]
  exact ⟨lt_mul_of_lt_of_one_le a_lt_n one_le_b, lt_mul_of_lt_of_one_le b_lt_n one_le_a⟩

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