mul_left_cancel_iff' — Mathlib

English

For all a,b,c,m, c ≠ 0, c·a ≡ c·b (mod c·m) iff a ≡ b (mod m).

Русский

Для всех a,b,c,m, c ≠ 0, c·a ≡ c·b (mod c·m) тогда и только тогда, что a ≡ b (mod m).

LaTeX

$$$ \forall a,b,c,m:\; c \neq 0 \Rightarrow (c a \equiv c b \pmod{c m} \iff a \equiv b \pmod{m}) $$$

Lean4

protected theorem mul_left_cancel_iff' {a b c m : ℕ} (hc : c ≠ 0) : c * a ≡ c * b [MOD c * m] ↔ a ≡ b [MOD m] :=
  ⟨ModEq.mul_left_cancel' hc, ModEq.mul_left' _⟩

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