sub_modEq_iff_modEq_add' — Mathlib

English

For nonzero n, a ≡ b (mod p) iff there exists i with 0 ≤ i < n such that a ≡ b + i p (mod n p).

Русский

Для ненулевого n существует i, 0 ≤ i < n, такое что a ≡ b + i p (mod n p) тогда и только тогда, когда a ≡ b (mod p).

LaTeX

$$$ n \\neq 0 \\Rightarrow \\big( a \\equiv b \\pmod{p} \\big) \\iff \\exists i < n,\\ a \\equiv b + i \\cdot p \\pmod{n \\cdot p} \\big)$$

Lean4

theorem sub_modEq_iff_modEq_add' : a - b ≡ c [PMOD p] ↔ a ≡ b + c [PMOD p] :=
  modEq_comm.trans <| modEq_sub_iff_add_modEq'.trans modEq_comm

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