Commit 2021-08-13 17:03 c711909c

View on Github →

feat(linear_algebra/basic, group_theory/quotient_group, algebra/lie/quotient): ext lemmas for morphisms out of quotients (#8641) This allows ext to see through quotients by subobjects of a type A, and apply ext lemmas specific to A.

Estimated changes

Modified src/algebra/category/Group/colimits.lean

Modified src/algebra/lie/basic.lean

added theorem lie_module_hom.congr_fun

Modified src/algebra/lie/quotient.lean

added theorem lie_submodule.quotient.lie_module_hom_ext

added def lie_submodule.quotient.mk'

Modified src/algebra/ring_quot.lean

Modified src/group_theory/quotient_group.lean

added theorem quotient_group.monoid_hom_ext

added theorem quotient_group.quotient_map_subgroup_of_of_le_coe

Modified src/linear_algebra/basic.lean

added theorem submodule.linear_map_qext

Modified src/ring_theory/ideal/basic.lean

added theorem ideal.quotient.ring_hom_ext