setoid — Mathlib

English

The relation of N-conjugacy on splittings induces an equivalence relation (setoid) on the split objects.

Русский

Отношение N-конъюгированности на разложениях порождает эквивалентность (setoid) на разложениях.

LaTeX

$$$S.IsConj \\text{ on } S.Splitting \\text{ is an equivalence relation}$$$

Lean4

/-- The setoid of splittings with `N`-conjugacy -/
@[to_additive /-- The setoid of splittings with `N`-conjugacy -/
    ]
def setoid : Setoid S.Splitting where
  r := S.IsConj
  iseqv :=
    { refl := refl S
      symm := symm S
      trans := trans S }

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