mul_modEq_mul_left — Mathlib

English

Similarly, multiplying by c on the left (when c ≠ 0) preserves modular equivalence up to modulus division by c.

Русский

Умножение слева на c сохранит модульную эквивалентность с делением модуля на c, при условии c ≠ 0.

LaTeX

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

Lean4

@[simp]
theorem mul_modEq_mul_left (hc : c ≠ 0) : c * a ≡ c * b [PMOD p] ↔ a ≡ b [PMOD (p / c)] := by simp [mul_comm c, hc]

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