commensurator_mem_iff — Mathlib

English

Membership in commensurator(H) is characterized by g ∈ G with (g • H) commensurable to H.

Русский

Членство в commensurator(H) определяется тем, что ∈ G и (g • H) комменсируемо с H.

LaTeX

$$g ∈ commensurator H ↔ Commensurable (ConjAct.toConjAct g • H) H$$

Lean4

@[simp]
theorem commensurator_mem_iff (H : Subgroup G) (g : G) :
    g ∈ commensurator H ↔ Commensurable (ConjAct.toConjAct g • H) H :=
  Iff.rfl

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