modEq_iff_toIcoMod_eq_left — Mathlib

English

For all z ∈ ℤ, b − z p is not in the open interval (a, a + p) if and only if a ≡ b (PMOD p).

Русский

Пусть для всех z ∈ ℤ верно: b − zp не принадлежит открытому интервалу (a, a + p) тогда и только если a эквивалентно b по модулю p.

LaTeX

$$$ a \\equiv b\\ [PMOD\\ p] \\iff \\forall z \\in \\mathbb{Z},\\ b - z \\cdot p \\notin (a, a + p) $$$

Lean4

theorem modEq_iff_toIcoMod_eq_left : a ≡ b [PMOD p] ↔ toIcoMod hp a b = a :=
  modEq_iff_eq_add_zsmul.trans
    ⟨by
      rintro ⟨n, rfl⟩
      rw [toIcoMod_add_zsmul, toIcoMod_apply_left], fun h => ⟨toIcoDiv hp a b, eq_add_of_sub_eq h⟩⟩

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