commensurator — Mathlib

English

Defines commensurator(H) as the pullback of commensurator'(H) along the ConjAct to Conjugation action.

Русский

Определяет commensurator(H) как вытяжку commensurator'(H) вдоль конъюгирующего действия.

LaTeX

$$commensurator (H) = commensurator'(H) .comap ConjAct.toConjAct.toMonoidHom$$

Lean4

/-- For `H` a subgroup of `G`, this is the subgroup of all elements `g : G`
such that `Commensurable (g H g⁻¹) H` -/
def commensurator (H : Subgroup G) : Subgroup G :=
  (commensurator' H).comap ConjAct.toConjAct.toMonoidHom

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