sub_floor_div_mul_lt — Mathlib

English

For m,n ∈ ℕ with n ≠ 0, fract((m/n)) = (m mod n)/n (after appropriate casts).

Русский

Для m,n ∈ ℕ, n ≠ 0, fract((m/n)) = (m mod n)/n (с соответствующими приведениями к тому же кольцу).

LaTeX

$$$\\\\operatorname{fract}(\\\\frac{m}{n}) = \\\\frac{m \\\\bmod n}{n}$$$

Lean4

theorem sub_floor_div_mul_lt (a : k) (hb : 0 < b) : a - ⌊a / b⌋ * b < b :=
  sub_lt_iff_lt_add.2 <| by
    rw [← one_add_mul, ← div_lt_iff₀ hb, add_comm]
    exact lt_floor_add_one _

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