modEq_iff_forall_notMem_Ioo_mod — Mathlib

English

For AddCommGroup, a ≡ b [PMOD p] holds if and only if for all integers z, b − z p ∉ Ioo a (a + p).

Русский

Для AddCommGroup: a ≡ b [PMOD p] эквивалентно тому, что для всякого z ∈ ℤ, b − z p ∉ Ioo a (a + p).

LaTeX

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

Lean4

theorem modEq_iff_forall_notMem_Ioo_mod : a ≡ b [PMOD p] ↔ ∀ z : ℤ, b - z • p ∉ Set.Ioo a (a + p) :=
  (tfae_modEq hp a b).out 0 1

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