Theorem Subgroup.index_map_of_injective

Modification history

2026-09-22 12:37
Mathlib/GroupTheory/Index.lean
feat(GroupTheory/Index): add Lagrange's theorem for monoid homomorphisms (#43845)
Modified Subgroup.index_map_of_injectiveView on Github →
2024-11-13 20:45
Mathlib/GroupTheory/Index.lean
feat(GroupTheory/Sylow): Surjective group homomorphisms map Sylow subgroups to Sylow subgroups (#18783) …
Added Subgroup.index_map_of_injectiveView on Github →