mathlib

077cd7c0 - feat(algebra/category/Algebra): basic setup for category of bundled R-algebras (#3047)

feat(algebra/category/Algebra): basic setup for category of bundled R-algebras (#3047) Just boilerplate. If I don't run out of enthusiasm I'll do tensor product of R-algebras soon. (#3050) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>