not_modEq_iff_ne_mod_zmultiples — Mathlib

English

Not A ≡ B (mod p) iff (A : α ⧸ zmultiples p) ≠ B.

Русский

Не A ≡ B (mod p) эквивалентно тому, что в факторгруппе по zmultiples p элементы A и B различны.

LaTeX

$$$ \\neg (a \\equiv b \\pmod{p}) \\iff (a : \\alpha \\!\\!\\! / AddSubgroup.zmultiples(p)) \\neq b $$$

Lean4

theorem not_modEq_iff_ne_mod_zmultiples : ¬a ≡ b [PMOD p] ↔ (a : α ⧸ AddSubgroup.zmultiples p) ≠ b :=
  modEq_iff_eq_mod_zmultiples.not

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