toMulDivCancelClass — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance (priority := 100) toMulDivCancelClass : MulDivCancelClass R where
  mul_div_cancel a b
    hb := by
    refine (eq_of_sub_eq_zero ?_).symm
    by_contra h
    have := mul_right_not_lt b h
    rw [sub_mul, mul_comm (_ / _), sub_eq_iff_eq_add'.2 (div_add_mod (a * b) b).symm] at this
    exact this (mod_lt _ hb)

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