Theorems · Definition · group theory

Subgroup.Commensurable.commensurator

{G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup G

For H a subgroup of G, this is the subgroup of all elements g : G such that Commensurable (g H g⁻¹) H

Defined in

Mathlib.GroupTheory.Commensurable

Cited by

7 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group