modEq_comm — Mathlib

English

In any additive abelian group, congruence modulo p is symmetric: a ≡ b (mod p) if and only if b ≡ a (mod p).

Русский

В любой аддитивной абелевой группе конгруэнтность по модулю p симметрична: a ≡ b (mod p) тогда и только тогда, когда b ≡ a (mod p).

LaTeX

$$$a \equiv b [PMOD p] \iff b \equiv a [PMOD p]$$$

Lean4

theorem modEq_comm : a ≡ b [PMOD p] ↔ b ≡ a [PMOD p] :=
  (Equiv.neg _).exists_congr_left.trans <| by simp [ModEq, ← neg_eq_iff_eq_neg]

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