Theorem Subgroup.NormalizerCondition.normal_of_coatom

Modification history

2024-07-01 22:27

Mathlib/Algebra/Group/Subgroup/Basic.lean

chore (Subgroup.Order): move ordered facts out of `Basic` and into `Order` (#14121) …

Modified Subgroup.NormalizerCondition.normal_of_coatom View on Github →

2023-01-26 10:26

Mathlib/GroupTheory/Subgroup/Basic.lean

feat: port GroupTheory.Subgroup.Basic (#1797)

Added Subgroup.NormalizerCondition.normal_of_coatom View on Github →