mod_lcm — Mathlib

English

If a ≡ b mod n and a ≡ b mod m, then a ≡ b mod lcm(n,m).

Русский

Если a ≡ b (mod n) и a ≡ b (mod m), то a ≡ b (mod lcm(n,m)).

LaTeX

$$$\\\\forall m,n\\\\in \\\\mathbb{N},\\\\ a \\\\equiv b \\\\pmod{n} \\\\land \\\\ a \\\\equiv b \\\\pmod{m} \\\\Rightarrow a \\\\equiv b \\\\pmod{\\\\mathrm{lcm}(n,m)}$$$

Lean4

theorem mod_lcm (hn : a ≡ b [MOD n]) (hm : a ≡ b [MOD m]) : a ≡ b [MOD lcm n m] :=
  Nat.modEq_iff_dvd.mpr <| Int.coe_lcm_dvd (Nat.modEq_iff_dvd.mp hn) (Nat.modEq_iff_dvd.mp hm)

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