Theorems · Definition · group theory

Subgroup.focalSubgroup

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

The Focal Subgroup of a subgroup H (denoted H* or foc(H)). It is generated by elements of the form x⁻¹ * (u * x * u⁻¹) where both x and x^u are in H.

Defined in

Mathlib.GroupTheory.Focal

Cited by

9 results in Mathlib

Foundations

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

Assumes

Group