mul_modEq_mul_right — Mathlib

English

In a division ring, multiplying both sides by c on the right preserves a mod-c relation, adjusting the modulus by dividing by c.

Русский

В делимом кольце умножение справа на c сохраняет модульную зависимость, модуль делится на c.

LaTeX

$$$ a \cdot c \equiv b \cdot c \ [PMOD p] \iff a \equiv b \ [PMOD (p / c)] $$$

Lean4

@[simp]
theorem mul_modEq_mul_right (hc : c ≠ 0) : a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD (p / c)] := by
  rw [div_eq_mul_inv, ← div_modEq_div (inv_ne_zero hc), div_inv_eq_mul, div_inv_eq_mul]

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