Def Module.monoidal_closed_hom_equiv

Modification history

2023-05-18 17:57
src/algebra/category/Module/monoidal/basic.lean
chore(algebra/category/Module/monoidal): split file (#19034)
Modified Module.monoidal_closed_hom_equivView on Github →
2022-03-04 08:56
src/algebra/category/Module/monoidal.lean
feat(algebra/category): Module R is monoidal closed for comm_ring R (#12387)
Added Module.monoidal_closed_hom_equivView on Github →