div_modEq_div — Mathlib

English

In a division ring, dividing both sides by a nonzero element c preserves modular equivalence up to scaling the modulus by c.

Русский

В делимой кольце деление обеих сторон на ненулевой элемент c сохраняет модульную эквивалентность при масштабировании модуля на c.

LaTeX

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

Lean4

@[simp]
theorem div_modEq_div (hc : c ≠ 0) : a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD (p * c)] := by
  simp [ModEq, ← sub_div, div_eq_iff hc, mul_assoc]

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