Commit 2026-04-05 08:02 69f07e41

View on Github →

chore(GroupTheory/Sylow): remove explicit type ascriptions (P : Subgroup G) (#37086) PR #36852 generalized normalizer to subsets of G (like we do for centralizer), but introduced a few explicit type ascriptions (P : Subgroup) into Sylow.lean (to force the coercion to Set to go through Subgroup). This PR removes those.

Estimated changes

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

modified theorem Subgroup.mem_normalizer_iff''

added theorem Subgroup.mem_set_normalizer_iff''

added theorem Subgroup.mem_set_normalizer_iff'

added theorem Subgroup.mem_set_normalizer_iff

Modified Mathlib/GroupTheory/SpecificGroups/ZGroup.lean

Modified Mathlib/GroupTheory/Sylow.lean

modified theorem Sylow.smul_eq_of_normal

Modified Mathlib/GroupTheory/Transfer.lean

modified theorem MonoidHom.transferSylow_restrict_eq_pow