of_dvd

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.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 \quad\text{and}\quad a \equiv b \pmod n\Rightarrow a \equiv b \pmod m$$$

Lean4

protected theorem of_dvd (d : m ∣ n) (h : a ≡ b [ZMOD n]) : a ≡ b [ZMOD m] :=
  modEq_iff_dvd.2 <| d.trans h.dvd

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

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

Разделы

Аффилиация

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