mathlib
0c64b3d3 - feat(algebra/category/Module): biproducts (#13908)

Commit
3 years ago
feat(algebra/category/Module): biproducts (#13908) Following the same pattern for `AddCommGroup`, create the instance for biproducts in` Module R`, and check they are isomorphic to the usual construction. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading