Commit 2024-07-01 22:27 b32cc985

View on Github →

chore (Subgroup.Order): move ordered facts out of Basic and into Order (#14121) We don't want to import the order hierarchy without really needing it.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

deleted theorem MulEquiv.isCoatom_comap

deleted theorem MulEquiv.isCoatom_map

deleted theorem Subgroup.NormalizerCondition.normal_of_coatom

deleted theorem Subgroup.isCoatom_comap_of_surjective

deleted theorem abs_mem_iff

Modified Mathlib/Algebra/Group/Subgroup/Order.lean

added theorem Subgroup.NormalizerCondition.normal_of_coatom

added theorem Subgroup.isCoatom_comap

added theorem Subgroup.isCoatom_comap_of_surjective

added theorem Subgroup.isCoatom_map

added theorem abs_mem_iff

Modified Mathlib/GroupTheory/Archimedean.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/Subgroup/Simple.lean