add_div_eq_of_add_mod_lt — Mathlib

English

If h : a ≡ b [MOD gcd n m], and n,m ≠ 0, then the constructed witness is strictly less than lcm(n,m).

Русский

Если h : a ≡ b (mod gcd(n,m)) и n,m ≠ 0, то построенный свидетель меньше чем lcm(n,m).

LaTeX

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

Lean4

theorem add_div_eq_of_add_mod_lt {a b c : ℕ} (hc : a % c + b % c < c) : (a + b) / c = a / c + b / c :=
  if hc0 : c = 0 then by simp [hc0]
  else by rw [Nat.add_div (Nat.pos_of_ne_zero hc0), if_neg (not_le_of_gt hc), add_zero]

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