mul_left_cancel' — Mathlib

English

If c ≠ 0 and c a ≡ c b (mod c m), then a ≡ b (mod m).

Русский

Если c ≠ 0 и c a ≡ c b (mod c m), то a ≡ b (mod m).

LaTeX

$$$c \\neq 0 \\Rightarrow (c a \\equiv c b [ZMOD c m]) \\Rightarrow a \\equiv b [ZMOD m].$$$

Lean4

/-- Cancel left multiplication on both sides of the `≡` and in the modulus.

For cancelling left multiplication in the modulus, see `Int.ModEq.of_mul_left`. -/
protected theorem mul_left_cancel' (hc : c ≠ 0) : c * a ≡ c * b [ZMOD c * m] → a ≡ b [ZMOD m] :=
  by
  simp only [modEq_iff_dvd, ← Int.mul_sub]
  exact Int.dvd_of_mul_dvd_mul_left hc

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