rightRel_eq — Mathlib

English

Right cosets are in bijection with left cosets; there is a canonical isomorphism between α / s defined by left and right relations.

Русский

Правые косеты эквивалентны левым косетам; существует каноническое биекция между двумя представлениями α / s.

LaTeX

$$Right cosets ≃ Left cosets; equivalence α / (rightRel s) ≃ α / (leftRel s)$$

Lean4

@[to_additive]
theorem rightRel_eq : ⇑(rightRel s) = fun x y => y * x⁻¹ ∈ s :=
  funext₂ <| by
    simp only [eq_iff_iff]
    apply rightRel_apply

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