comm — Mathlib

English

For any H, K and any g in G, H and K are commensurable if and only if gHg⁻¹ and gKg⁻¹ are commensurable.

Русский

Для любых подгрупп H, K и элемента g группы G верно: H и K комменсурируемы тогда и только тогда, когда их конъюгированные группы gHg⁻¹ и gKg⁻¹ комменсурируемы.

LaTeX

$$Commensurable H K ↔ Commensurable (g • H) (g • K)$$

Lean4

@[to_additive]
theorem comm {H K : Subgroup G} : Commensurable H K ↔ Commensurable K H :=
  and_comm

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