mathlib3

c711909c - feat(linear_algebra/basic, group_theory/quotient_group, algebra/lie/quotient): ext lemmas for morphisms out of quotients (#8641)

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`.