Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-28 16:55 781d1875

View on Github →

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

Estimated changes

Modified src/group_theory/quotient_group.lean

modified theorem quotient_group.injective_ker_lift

added def quotient_group.ker_lift

added theorem quotient_group.ker_lift_mk'

added theorem quotient_group.ker_lift_mk