mathlib
820f8d72 - feat(group_theory/index): Index of `subgroup.map` (#10232)

Commit

4 years ago

feat(group_theory/index): Index of `subgroup.map` (#10232) Proves `(H.map f).index = H.index`, assuming `function.surjective f` and `f.ker ≤ H`.

Author

tb65536

Parents