Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-08 18:57 9d40a598

View on Github →

feat(group_theory,linear_algebra): third isomorphism theorem for groups and modules (#8203) This PR proves the third isomorphism theorem for (additive) groups and modules, and also adds a few simp lemmas that I needed.

Estimated changes

Modified docs/overview.yaml

Modified src/group_theory/quotient_group.lean

added theorem quotient_group.map_coe

added theorem quotient_group.map_mk'

added def quotient_group.quotient_quotient_equiv_quotient

added def quotient_group.quotient_quotient_equiv_quotient_aux

added theorem quotient_group.quotient_quotient_equiv_quotient_aux_coe

added theorem quotient_group.quotient_quotient_equiv_quotient_aux_coe_coe

Modified src/linear_algebra/basic.lean

added def submodule.quotient_quotient_equiv_quotient

added def submodule.quotient_quotient_equiv_quotient_aux

added theorem submodule.quotient_quotient_equiv_quotient_aux_mk

added theorem submodule.quotient_quotient_equiv_quotient_aux_mk_mk