mathlib

a574db13 - refactor(algebra/category/*/limits): refactor concrete limits (#3463)

refactor(algebra/category/*/limits): refactor concrete limits (#3463) We used to construct categorical limits for `AddCommGroup` and `CommRing`. Now we construct them for * `(Add)(Comm)Mon` * `(Add)(Comm)Group` * `(Comm)(Semi)Ring` * `Module R` * `Algebra R` Even better, we reuse structure along the way, and show that all the relevant forgetful functors preserve limits. We're still not at the point were this can either be done by * automation, or * noticing that everything is a model of a Lawvere theory but ... maybe one day. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>