mod_nat_eq_sub_mul_floor_rat_div — Mathlib

English

For any integer n and natural d, n mod d equals n minus d times floor((n/d) in ℚ); i.e. n % d = n − d ⌊(n:ℚ)/d⌋.

Русский

Для любого целого n и натурального d, n mod d равно n минус d умноженное на ⌊(n:d)⌋ в ℚ; то есть n % d = n − d ⌊(n:ℚ)/d⌋.

LaTeX

$$$$ n \\% d = n - d \\left\\lfloor \\frac{n}{d} \\right\\rfloor \\quad (n \\in \\mathbb{Z},\\ d \\in \\mathbb{N}). $$$$

Lean4

theorem mod_nat_eq_sub_mul_floor_rat_div {n : ℤ} {d : ℕ} : n % d = n - d * ⌊(n : ℚ) / d⌋ := by
  rw [Int.emod_def, Rat.floor_intCast_div_natCast]

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