mod_eq_sub_mul_div — Mathlib

English

In a Euclidean domain, the remainder satisfies a % b = a − b · (a / b).

Русский

В евклидовом домене остаток удовлетворяет a mod b = a − b · (a / b).

LaTeX

$$$ a \% b = a - b \cdot (a / b) $$$

Lean4

theorem mod_eq_sub_mul_div {R : Type*} [EuclideanDomain R] (a b : R) : a % b = a - b * (a / b) :=
  calc
    a % b = b * (a / b) + a % b - b * (a / b) := (add_sub_cancel_left _ _).symm
    _ = a - b * (a / b) := by rw [div_add_mod]

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