mathlib3
781d1875 - feat(group_theory/quotient_group): define ker_lift and prove simp-lemmas (#764)

Commit

6 years ago

feat(group_theory/quotient_group): define ker_lift and prove simp-lemmas (#764) * feat(group_theory/quotient_group): define ker_lift and prove simp-lemmas * Add docstring

References

#764 - feat(group_theory/quotient_group): define ker_lift and prove simp-lemmas

Author

jcommelin

Committer

ChrisHughes24

Parents

81f85308

mathlib3 781d1875 - feat(group_theory/quotient_group): define ker_lift and prove simp-lemmas (#764)

mathlib3
781d1875 - feat(group_theory/quotient_group): define ker_lift and prove simp-lemmas (#764)