Theorem MonoidHom.transferSylow_restrict_eq_pow

Modification history

2026-07-20 01:34
Mathlib/GroupTheory/Transfer.lean
refactor: rename restrict to domRestrict (#25980) …
Deleted MonoidHom.transferSylow_restrict_eq_powView on Github →
2026-04-05 08:02
Mathlib/GroupTheory/Transfer.lean
chore(GroupTheory/Sylow): remove explicit type ascriptions `(P : Subgroup G)` (#37086) …
Modified MonoidHom.transferSylow_restrict_eq_powView on Github →
2023-06-05 17:06
Mathlib/GroupTheory/Transfer.lean
feat: port GroupTheory.Transfer (#4482)
Added MonoidHom.transferSylow_restrict_eq_powView on Github →