add_mod_of_add_mod_lt — Mathlib

English

If z ≡ a mod n and z ≡ b mod m with gcd(n,m)=1, then z ≡ ChineseRemainder(n,m;a,b) mod nm.

Русский

Если z ≡ a mod n и z ≡ b mod m при gcd(n,m)=1, то z ≡ ChineseRemainder(n,m;a,b) mod nm.

LaTeX

$$$\\\\forall n,m \\\\in \\\\mathbb{N},\\\\ gcd(n,m)=1 \\\\Rightarrow \\\\forall a,b,z \\\\in \\\\mathbb{N},\\\\ z \\\\equiv a \\\\pmod{n} \\\\land \\\\ z \\\\equiv b \\\\pmod{m} \\\\Rightarrow \\\\ z \\\\equiv \\text{ChineseRemainder}(n,m;a,b) \\\\pmod{nm}$$$

Lean4

theorem add_mod_of_add_mod_lt {a b c : ℕ} (hc : a % c + b % c < c) : (a + b) % c = a % c + b % c := by
  rw [← add_mod_add_ite, if_neg (not_le_of_gt hc), add_zero]

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