eq — Mathlib · SciLib

English

If H and K are commensurable, then their commensurators coincide: commensurator H = commensurator K.

Русский

Если H и K комменсурируемы, то их комменсураторы совпадают: commensurator(H) = commensurator(K).

LaTeX

$$Commensurable H K → commensurator H = commensurator K$$

Lean4

theorem eq {H K : Subgroup G} (hk : Commensurable H K) : commensurator H = commensurator K :=
  Subgroup.ext fun x =>
    let hx := (commensurable_conj x).1 hk
    ⟨fun h => hx.symm.trans (h.trans hk), fun h => hx.trans (h.trans hk.symm)⟩

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