def — Mathlib

English

Two elements are equivalent modulo U iff their difference lies in U; this is the symmetry of the congruence relation modulo U.

Русский

Два элемента эквивалентны по отношению к U тогда и только тогда их разность лежит в U; это симметрия эквиваленции по модулю U.

LaTeX

$$$ x \\equiv y \\;[\\mathrm{SMOD}\\; U] \\;\\iff\\; x-y \\in U$$$

Lean4

protected theorem «def» : x ≡ y [SMOD U] ↔ (Submodule.Quotient.mk x : M ⧸ U) = Submodule.Quotient.mk y :=
  Iff.rfl

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