Commit 2023-07-27 07:08 13e7c2f0

View on Github →

chore(GroupTheory): forward-port leanprover-community/mathlib#18965 (#6147)

Estimated changes

Modified Mathlib/GroupTheory/Abelianization.lean

Modified Mathlib/GroupTheory/Commutator.lean

modified theorem Subgroup.commutator_eq_bot_iff_le_centralizer

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

modified theorem ConjAct.stabilizer_eq_centralizer

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

modified def Subgroup.centralizer

modified theorem Subgroup.centralizer_eq_top_iff_subset

modified theorem Subgroup.centralizer_le

deleted theorem Subgroup.centralizer_top

added theorem Subgroup.centralizer_univ

modified theorem Subgroup.le_centralizer

modified theorem Subgroup.le_centralizer_iff

modified theorem Subgroup.le_centralizer_iff_isCommutative

modified theorem Subgroup.mem_centralizer_iff

modified theorem Subgroup.mem_centralizer_iff_commutator_eq_one

Modified Mathlib/GroupTheory/Subgroup/ZPowers.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/GroupTheory/Transfer.lean