add_mod_add_of_le_add_mod — Mathlib

English

If a ≡ b modulo gcd(n,m) and n,m ≠ 0, then the witness k produced by ChineseRemainder' satisfies k < lcm(n,m).

Русский

Если a ≡ b по gcd(n,m) и n,m ≠ 0, то найденный элемент k удовлетворяет k < lcm(n,m).

LaTeX

$$$\\\\forall m,n \\\\in \\\\mathbb{N},\\\\ a \\\\equiv b \\\\pmod{\\\\gcd(n,m)} \\\\land \\\\ n \\\\neq 0 \\\\land \\\\ m \\\\neq 0 \\\\Rightarrow \\\\text{(chineseRemainder'(a,b; n,m)).val} < \\mathrm{lcm}(n,m)$$$

Lean4

theorem add_mod_add_of_le_add_mod {a b c : ℕ} (hc : c ≤ a % c + b % c) : (a + b) % c + c = a % c + b % c := by
  rw [← add_mod_add_ite, if_pos hc]

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