quotientRel — Mathlib

English

The quotient relation associated to a submodule p is defined by x ~ y iff -x + y ∈ p, equivalently y − x ∈ p.

Русский

Отношение эквивалентности, порождаемое подмодулем p, задаётся как x ~ y тогда и только тогда, когда -x + y ∈ p, эквивалентно y − x ∈ p.

LaTeX

$$$x \sim y \;\iff\; x - y \in p.$$$

Lean4

/-- The equivalence relation associated to a submodule `p`, defined by `x ≈ y` iff `-x + y ∈ p`.

Note this is equivalent to `y - x ∈ p`, but defined this way to be defeq to the `AddSubgroup`
version, where commutativity can't be assumed. -/
def quotientRel : Setoid M :=
  QuotientAddGroup.leftRel p.toAddSubgroup

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