mathlib3

feat(category_theory/*): Monoid objects in Abelian group are rings

#17006

Open