rightRel — Mathlib

English

Right cosets partition a group in the same way as left cosets, with the relation x ~ y defined by y x^{-1} ∈ s.

Русский

Правая косета образует аналогичное разбиение группы; отношение x ~ y задано как y x^{-1} ∈ s.

LaTeX

$$$x \sim_R y \iff y x^{-1} \in s$$$

Lean4

/-- The equivalence relation corresponding to the partition of a group by right cosets of a
subgroup. -/
@[to_additive /-- The equivalence relation corresponding to the partition of a group by right cosets
    of a subgroup. -/
    ]
def rightRel : Setoid α :=
  MulAction.orbitRel s α

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