mulLeftCosetsCompSubtypeVal — Mathlib

English

There is a natural action of a subgroup I on the left coset space α/H given by conjugation through a subgroup-subtype map.

Русский

Существует естественное действие подгруппы I на множестве левых косет α/H через отображение подгруппы и типа.

LaTeX

$$$\\text{MulAction}\\; I\\; (\\alpha \\backslash H) = \\text{MulAction}((\\text{Subtype}\\; I), \\alpha/H)$$$

Lean4

@[to_additive]
instance mulLeftCosetsCompSubtypeVal (H I : Subgroup α) : MulAction I (α ⧸ H) :=
  MulAction.compHom (α ⧸ H) (Subgroup.subtype I)

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