Mathlib v3 is deprecated. Go to Mathlib v4

Def quotient_group.quotient_ker_equiv_of_right_inverse

Modification history

2022-12-30 06:17
src/group_theory/quotient_group.lean
chore(group_theory/quotient_group): open `function`, use `rfl` (#18014)
Modified quotient_group.quotient_ker_equiv_of_right_inverseView on Github →
2021-06-18 23:32
src/group_theory/quotient_group.lean
feat(group_theory): computable 1st isomorphism theorem (#7988) …
Added quotient_group.quotient_ker_equiv_of_right_inverseView on Github →