mathlib

03b88c14 - feat(algebra/category/Module): Free R C, the free R-linear completion of a category (#7177)

feat(algebra/category/Module): Free R C, the free R-linear completion of a category (#7177) The free R-linear completion of a category. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com>