modEq_iff_toIocMod_eq_right — Mathlib

English

A ≡ B (PMOD p) if and only if toIocMod hp a b = a + p.

Русский

A ≡ B (PMOD p) эквивалентно toIocMod hp a b = a + p.

LaTeX

$$$ a \\equiv b\\ [PMOD\\ p] \\iff toIocMod\\ hp\\ a\\ b = a + p $$$

Lean4

theorem modEq_iff_toIocMod_eq_right : a ≡ b [PMOD p] ↔ toIocMod hp a b = a + p :=
  by
  refine modEq_iff_eq_add_zsmul.trans ⟨?_, fun h => ⟨toIocDiv hp a b + 1, ?_⟩⟩
  · rintro ⟨z, rfl⟩
    rw [toIocMod_add_zsmul, toIocMod_apply_left]
  · rwa [add_one_zsmul, add_left_comm, ← sub_eq_iff_eq_add']

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