leftCosetEquivSubgroup — Mathlib

English

There is a natural bijection between the left coset g s and the subgroup s, given by h maps to g^{-1} h.

Русский

Существует естественная биекция между левой косетой g s и подгруппой s, задаваемая h ↦ g^{-1} h.

LaTeX

$$$(g\,s) \cong s \quad\text{via}\quad h \mapsto g^{-1} h$$$

Lean4

/-- The natural bijection between a left coset `g * s` and `s`. -/
@[to_additive /-- The natural bijection between the cosets `g + s` and `s`. -/
    ]
def leftCosetEquivSubgroup (g : α) : (g • s : Set α) ≃ s :=
  ⟨fun x => ⟨g⁻¹ * x.1, (mem_leftCoset_iff _).1 x.2⟩, fun x => ⟨g * x.1, x.1, x.2, rfl⟩, fun ⟨x, _⟩ =>
    Subtype.eq <| by simp, fun ⟨g, _⟩ => Subtype.eq <| by simp⟩

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