Commit 2023-07-06 04:18 15a4f796

View on Github →

feat: port CategoryTheory.Monoidal.Internal.Module (#5725)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Internal/Module.lean

added theorem ModuleCat.MonModuleEquivalenceAlgebra.algebraMap

added def ModuleCat.MonModuleEquivalenceAlgebra.functor

added def ModuleCat.MonModuleEquivalenceAlgebra.inverse

added def ModuleCat.MonModuleEquivalenceAlgebra.inverseObj

added def ModuleCat.monModuleEquivalenceAlgebra

added def ModuleCat.monModuleEquivalenceAlgebraForget