Def FGModuleCat.forget₂Monoidal

Modification history

2024-11-10 22:57
Mathlib/Algebra/Category/FGModuleCat/Basic.lean
refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal (#17904) …
Deleted FGModuleCat.forget₂MonoidalView on Github →
2023-06-26 04:12
Mathlib/Algebra/Category/FGModuleCat/Basic.lean
feat: port Algebra.Category.FGModule.basic (#4878) …
Added FGModuleCat.forget₂MonoidalView on Github →