mul_right_cancel' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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

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