mathlib3
9beec03c - feat(group_theory/subgroup): le_ker_iff (#6630)

Commit

5 years ago

feat(group_theory/subgroup): le_ker_iff (#6630) A subgroup is contained in the kernel iff it is mapped to the trivial subgroup.

Author

tb65536

Parents