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 \quad \Rightarrow \quad (c a \equiv c b \pmod{c m}) \Rightarrow a \equiv b \pmod{m} $$$

Lean4

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

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

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