mathlib
9fec8f35 - feat(group_theory/index): `index_comap_of_surjective` (#9768)

Commit

4 years ago

feat(group_theory/index): `index_comap_of_surjective` (#9768) `subgroup.index` is preserved by `subgroup.comap`, provided that the homomorphism is surjective.

Author

tb65536

Parents

85f36400

mathlib 9fec8f35 - feat(group_theory/index): `index_comap_of_surjective` (#9768)

mathlib
9fec8f35 - feat(group_theory/index): `index_comap_of_surjective` (#9768)