of_mul_left — Mathlib

English

Cancel left multiplication in the modulus: from a ≡ b (mod m·n) deduce a ≡ b (mod n).

Русский

Отмена левого умножения в модуле: из a ≡ b (mod m·n) следует a ≡ b (mod n).

LaTeX

$$$ (m n) \mid (a - b) \Rightarrow n \mid (a - b) $? \;\text{more precisely:}\; a \equiv b \pmod{m n} \Rightarrow a \equiv b \pmod{n} $$$

Lean4

/-- Cancel left multiplication in the modulus.

For cancelling left multiplication on both sides of the `≡`, see `nat.modeq.mul_left_cancel'`. -/
theorem of_mul_left (m : ℕ) (h : a ≡ b [MOD m * n]) : a ≡ b [MOD n] :=
  by
  rw [modEq_iff_dvd] at *
  exact (dvd_mul_left (n : ℤ) (m : ℤ)).trans h

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