modEq_iff_eq_add_zsmul — Mathlib

English

A ≡ B (mod p) iff there exists an integer z such that B = A + z p.

Русский

A ≡ B (mod p) эквивалентно существованию целого z, такого что B = A + z p.

LaTeX

$$$ a \\equiv b \\pmod{p} \\iff \\exists z \\in \\mathbb{Z}, \\ b = a + z \\cdot p $$$

Lean4

theorem modEq_iff_eq_add_zsmul : a ≡ b [PMOD p] ↔ ∃ z : ℤ, b = a + z • p := by
  simp_rw [ModEq, sub_eq_iff_eq_add']
    -- this roughly matches `Int.modEq_zero_iff_dvd`

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