Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-18 17:57 74403a3b

View on Github →

chore(algebra/category/Module/monoidal): split file (#19034)

Estimated changes

Modified src/algebra/category/Module/adjunctions.lean

Renamed src/algebra/category/Module/monoidal.lean to src/algebra/category/Module/monoidal/basic.lean

deleted def Module.braiding

deleted theorem Module.braiding_naturality

deleted theorem Module.hexagon_forward

deleted theorem Module.hexagon_reverse

deleted theorem Module.ihom_coev_app

deleted theorem Module.ihom_ev_app

deleted theorem Module.ihom_map_apply

deleted theorem Module.monoidal_category.braiding_hom_apply

deleted theorem Module.monoidal_category.braiding_inv_apply

deleted theorem Module.monoidal_closed_curry

deleted def Module.monoidal_closed_hom_equiv

deleted theorem Module.monoidal_closed_pre_app

deleted theorem Module.monoidal_closed_uncurry

Created src/algebra/category/Module/monoidal/closed.lean

added theorem Module.ihom_coev_app

added theorem Module.ihom_ev_app

added theorem Module.ihom_map_apply

added theorem Module.monoidal_closed_curry

added def Module.monoidal_closed_hom_equiv

added theorem Module.monoidal_closed_pre_app

added theorem Module.monoidal_closed_uncurry

Created src/algebra/category/Module/monoidal/symmetric.lean

added def Module.braiding

added theorem Module.monoidal_category.braiding_hom_apply

added theorem Module.monoidal_category.braiding_inv_apply

added theorem Module.monoidal_category.braiding_naturality

added theorem Module.monoidal_category.hexagon_forward

added theorem Module.monoidal_category.hexagon_reverse

Modified src/algebra/category/fgModule/basic.lean

Modified src/category_theory/monoidal/internal/Module.lean

Modified src/representation_theory/Rep.lean