Theorem Subgroup.card_ker_mul_card_of_surjective

Modification history

2026-09-22 12:37
Mathlib/GroupTheory/Index.lean
feat(GroupTheory/Index): add Lagrange's theorem for monoid homomorphisms (#43845)
Added Subgroup.card_ker_mul_card_of_surjectiveView on Github →