RightCosetEquivalence — Mathlib

English

Equality of right cosets s·a and s·b is captured by op a • s = op b • s.

Русский

Равенство правых косет задается как s·a = s·b через эквивалентность op a • s = op b • s.

LaTeX

$$RightCosetEquivalence(s,a,b) := (op a)•s = (op b)•s$$

Lean4

/-- Equality of two right cosets `s * a` and `s * b`. -/
@[to_additive RightAddCosetEquivalence /-- Equality of two right cosets `s + a` and `s + b`. -/
    ]
def RightCosetEquivalence (s : Set α) (a b : α) :=
  op a • s = op b • s

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