not_modEq_iff_toIcoMod_eq_toIocMod

English

The negation of ModEq is equivalent to equality of IcoMod and IocMod: ¬a ≡ b [PMOD p] ↔ toIcoMod hp a b = toIocMod hp a b.

Русский

Отрицание ModEq эквивалентно равенству IcoMod и IocMod: ¬a ≡ b [PMOD p] ↔ toIcoMod hp a b = toIocMod hp a b.

LaTeX

$$$ \\neg (a \\equiv b\\ [PMOD\\ p]) \\iff toIcoMod\\ hp\\ a\\ b = toIocMod\\ hp\\ a\\ b $$$

Lean4

theorem not_modEq_iff_toIcoMod_eq_toIocMod : ¬a ≡ b [PMOD p] ↔ toIcoMod hp a b = toIocMod hp a b :=
  (modEq_iff_toIcoMod_ne_toIocMod _).not_left

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