of_div — Mathlib

English

If (a/c) ≡ (b/c) (mod m/c) and c | a, c | b, c | m, then a ≡ b (mod m).

Русский

Если (a/c) ≡ (b/c) (mod m/c) и c делит a, b и m, то a ≡ b (mod m).

LaTeX

$$$ (a/c) \equiv (b/c) \pmod{m/c} \land c \mid a \land c \mid b \land c \mid m \Rightarrow a \equiv b \pmod{m} $$$

Lean4

theorem of_div (h : a / c ≡ b / c [MOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) : a ≡ b [MOD m] := by
  convert h.mul_left' c <;> rwa [Nat.mul_div_cancel']

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