mathlib
fcd0f11c - feat(category_theory/flat_functor): Generalize results into algebraic categories. (#10735)

Commit

4 years ago

feat(category_theory/flat_functor): Generalize results into algebraic categories. (#10735) Also proves that the identity is flat, and compositions of flat functors are flat.

Author

erdOne

Parents

06905422

mathlib fcd0f11c - feat(category_theory/flat_functor): Generalize results into algebraic categories. (#10735)

mathlib
fcd0f11c - feat(category_theory/flat_functor): Generalize results into algebraic categories. (#10735)