Theorems · Definition · group theory

AddSubgroup.focalAddSubgroup

{G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → AddSubgroup 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

7 results in Mathlib

Foundations

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

Assumes

AddGroup