Commit 2025-11-06 23:28 6f5d80b4

View on Github →

chore(Algebra/Group/Subgroup): deprecate sup_subgroupOf_eq (#28389)

Estimated changes

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

modified theorem Subgroup.subgroupOf_sup

deleted theorem Subgroup.sup_subgroupOf_eq

Modified Mathlib/GroupTheory/PGroup.lean