leftCosetEquivalence_rel — Mathlib

English

The relation R(a,b) holds exactly when a•s = b•s, forming an equivalence relation on all group elements.

Русский

Отношение равно a•s = b•s образует эквивалентность на всех элементах группы.

LaTeX

$$Equivalence (LeftCosetEquivalence s)$$

Lean4

@[to_additive leftAddCosetEquivalence_rel]
theorem leftCosetEquivalence_rel (s : Set α) : Equivalence (LeftCosetEquivalence s) :=
  @Equivalence.mk _ (LeftCosetEquivalence s) (fun _ => rfl) Eq.symm Eq.trans

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