English
Two elements x,y ∈ α are related by the left coset relation with respect to s exactly when x⁻¹y ∈ s; this relation partitions α into left cosets xs.
Русский
Два элемента x,y ∈ α относятся друг к другу по левой косете относительно s тогда и только тогда, когда x⁻¹y ∈ s; это отношение разбивает α на левые косеты xs.
LaTeX
$$$x \sim_{\!s} y \quad\text{iff}\quad x^{-1} y \in s$$$
Lean4
/-- The equivalence relation corresponding to the partition of a group by left cosets
of a subgroup. -/
@[to_additive /-- The equivalence relation corresponding to the partition of a group by left cosets
of a subgroup. -/
]
def leftRel : Setoid α :=
MulAction.orbitRel s.op α
