of_mul_left

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.ModEq.of_mul_left

English

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

Русский

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

LaTeX

$$a ≡ b \pmod{m n} \Rightarrow a \equiv b \pmod n$$

Lean4

theorem of_mul_left (m : ℤ) (h : a ≡ b [ZMOD m * n]) : a ≡ b [ZMOD n] := by rw [modEq_iff_dvd] at *;
  exact (dvd_mul_left n m).trans h

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

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

Разделы

Аффилиация

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