Theorem Sylow.coe_equivProdPrimeFactors_apply

Modification history

2026-07-16 05:00
Mathlib/GroupTheory/Sylow.lean
feat(GroupTheory/PGroup): expand p-group API (#40143) …
Added Sylow.coe_equivProdPrimeFactors_applyView on Github →