quotientRel_def — Mathlib

English

The quotient relation is exactly the relation x ~ y iff x − y ∈ p, where p is the submodule and 0 is the neutral element.

Русский

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

LaTeX

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

Lean4

theorem quotientRel_def {x y : M} : p.quotientRel x y ↔ x - y ∈ p :=
  Iff.trans
    (by
      rw [leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]
      rfl)
    neg_mem_iff

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