rightCosetEquivSubgroup — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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