mathlib3

e053bdab - feat(category_theory/monoidal/internal): Mon_ (Module R) ≌ Algebra R (#3695)

feat(category_theory/monoidal/internal): Mon_ (Module R) ≌ Algebra R (#3695) The category of internal monoid objects in `Module R` is equivalent to the category of "native" bundled `R`-algebras. Moreover, this equivalence is compatible with the forgetful functors to `Module R`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>