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, и c делит b, и c делит m, тогда a ≡ b (mod m).

LaTeX

$$$(a / c) \\equiv (b / c) [ZMOD m / c] \\land c \\mid a \\land c \\mid b \\land c \\mid m \\Rightarrow a \\equiv b [ZMOD m].$$$

Lean4

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

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