English
We define modDiv(m,k) to be (m % k, m / k) with the same interpretation as in natural numbers, using the auxiliary modDivAux. This ensures m = (m % k) + k · (m / k).
Русский
Определим modDiv(m,k) как (m % k, m / k) по той же трактовке, что и в ℕ, через вспомогательную modDivAux. Это обеспечивает тождество m = (m % k) + k · (m / k).
LaTeX
$$$\\operatorname{modDiv}(m,k) = (m \\bmod k, m \\div k)$$$
Lean4
/-- `mod_div m k = (m % k, m / k)`.
We define `m % k` and `m / k` in the same way as for `ℕ`
except that when `m = n * k` we take `m % k = k` and
`m / k = n - 1`. This ensures that `m % k` is always positive
and `m = (m % k) + k * (m / k)` in all cases. Later we
define a function `div_exact` which gives the usual `m / k`
in the case where `k` divides `m`.
-/
def modDiv (m k : ℕ+) : ℕ+ × ℕ :=
modDivAux k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ))
