mathlib3
67b5ff6f - feat(algebra/direct_sum): constructor for morphisms into direct sums (#5204)

Commit

5 years ago

feat(algebra/direct_sum): constructor for morphisms into direct sums (#5204)

Author

jcommelin

jcommelin

Parents

Loading