English
Defines the commensurator' of H as the subgroup of g in ConjAct G such that (g • H) is commensurable with H.
Русский
Определяет комменсуратора' для H как подгруппу g в ConjAct G such that (g • H) комменсируемо с H.
LaTeX
$$commensurator' (H) : Subgroup (ConjAct G) = {g | Commensurable (g • H) H}$$
Lean4
/-- For `H` a subgroup of `G`, this is the subgroup of all elements `g : conjAut G`
such that `Commensurable (g • H) H` -/
def commensurator' (H : Subgroup G) : Subgroup (ConjAct G)
where
carrier := {g : ConjAct G | Commensurable (g • H) H}
one_mem' := by rw [Set.mem_setOf_eq, one_smul]
mul_mem' ha
hb := by
rw [Set.mem_setOf_eq, mul_smul]
exact trans ((commensurable_conj _).mp hb) ha
inv_mem' _ := by rwa [Set.mem_setOf_eq, comm, ← commensurable_inv]
