English
The natural-number remainder modulo k matches the defined remainder, i.e., (m mod k) in ℕ equals k if m ≡ 0 mod k, otherwise it equals (m mod k) as a natural number.
Русский
Остаток по модулю k совпадает с определенным остатком: если m ≡ 0 (mod k), то остаток равен k, иначе — обычный остаток m mod k.
LaTeX
$$$(m \\bmod k : \\mathbb{N}) = \\begin{cases} k, & (m \\bmod k) = 0 \\ (m \\bmod k), & (m \\bmod k)
eq 0 \\end{cases}$$$
Lean4
theorem mod_coe (m k : ℕ+) : (mod m k : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) (k : ℕ) ((m : ℕ) % (k : ℕ)) :=
by
dsimp [mod, modDiv]
cases (m : ℕ) % (k : ℕ) with
| zero =>
rw [if_pos rfl]
rfl
| succ n =>
rw [if_neg n.succ_ne_zero]
rfl
