mul_right_cancel' — Mathlib

English

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

Русский

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

LaTeX

$$$ c \neq 0 \Rightarrow (a c \equiv b c \pmod{m c}) \Rightarrow a \equiv b \pmod{m} $$$

Lean4

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

For cancelling right multiplication in the modulus, see `Nat.ModEq.of_mul_right`. -/
protected theorem mul_right_cancel' {a b c m : ℕ} (hc : c ≠ 0) : a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m] :=
  by
  simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.sub_mul]
  exact fun h => (Int.dvd_of_mul_dvd_mul_right (Int.ofNat_ne_zero.mpr hc) h)

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