mathlib3
23373d15 - chore(category_theory/limits): coproduct functor (#5677)

Commit

4 years ago

chore(category_theory/limits): coproduct functor (#5677) Dualises a def already there. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author

b-mehta

Parents