of_dvd

Mathlib.Data.Nat.ModEq

URI: https://scilib.ai/kg/mathlib#Nat.ModEq.of_dvd

English

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

Русский

Если m делит n и a ≡ b (mod n), тогда a ≡ b (mod m).

LaTeX

$$$m \mid n \\land a \\equiv b \\pmod{n} \\Rightarrow a \\equiv b \\pmod{m}$$$

Lean4

theorem of_dvd (d : m ∣ n) (h : a ≡ b [MOD n]) : a ≡ b [MOD m] :=
  modEq_of_dvd <| Int.ofNat_dvd.mpr d |>.trans h.dvd

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru