mathlib

106ac8e0 - feat(category_theory): definition of R-linear category (#7321)

feat(category_theory): definition of R-linear category (#7321) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>