setoid — Mathlib

English

There is a setoid on M × S given by the relation r, used to form the localization by quotienting.

Русский

Существует множество отношений (setoid) на M × S, заданное отношением r, которое используется для образования локализации через фактор-модуляцию.

LaTeX

$$$\\text{Setoid}(M \\times S, r_S^M)$.$$

Lean4

instance setoid : Setoid (M × S) where
  r := r S M
  iseqv :=
    ⟨(r.isEquiv S M).refl, (r.isEquiv S M).symm _ _, (r.isEquiv S M).trans _ _ _⟩
      -- TODO: change `Localization` to use `r'` instead of `r` so that the two types are also defeq,
      -- `Localization S = LocalizedModule S R`.

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