Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-01 00:04 e053bdab

View on Github →

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.

Estimated changes