Commit 2023-03-21 13:00 4fb0f4b5

View on Github →

feat: port CategoryTheory.Closed.Monoidal (#3002)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Closed/Monoidal.lean

added theorem CategoryTheory.MonoidalClosed.coev_app_comp_pre_app

added def CategoryTheory.MonoidalClosed.curry

added theorem CategoryTheory.MonoidalClosed.curry_eq

added theorem CategoryTheory.MonoidalClosed.curry_eq_iff

added theorem CategoryTheory.MonoidalClosed.curry_id_eq_coev

added theorem CategoryTheory.MonoidalClosed.curry_injective

added theorem CategoryTheory.MonoidalClosed.curry_natural_left

added theorem CategoryTheory.MonoidalClosed.curry_natural_right

added theorem CategoryTheory.MonoidalClosed.curry_uncurry

added theorem CategoryTheory.MonoidalClosed.eq_curry_iff

added theorem CategoryTheory.MonoidalClosed.homEquiv_apply_eq

added theorem CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq

added theorem CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev

added def CategoryTheory.MonoidalClosed.internalHom

added def CategoryTheory.MonoidalClosed.pre

added theorem CategoryTheory.MonoidalClosed.pre_comm_ihom_map

added theorem CategoryTheory.MonoidalClosed.pre_id

added theorem CategoryTheory.MonoidalClosed.pre_map

added def CategoryTheory.MonoidalClosed.uncurry

added theorem CategoryTheory.MonoidalClosed.uncurry_curry

added theorem CategoryTheory.MonoidalClosed.uncurry_eq

added theorem CategoryTheory.MonoidalClosed.uncurry_id_eq_ev

added theorem CategoryTheory.MonoidalClosed.uncurry_injective

added theorem CategoryTheory.MonoidalClosed.uncurry_natural_left

added theorem CategoryTheory.MonoidalClosed.uncurry_natural_right

added theorem CategoryTheory.MonoidalClosed.uncurry_pre

added def CategoryTheory.ihom.adjunction

added def CategoryTheory.ihom.coev

added theorem CategoryTheory.ihom.coev_ev

added theorem CategoryTheory.ihom.coev_naturality

added def CategoryTheory.ihom.ev

added theorem CategoryTheory.ihom.ev_coev

added theorem CategoryTheory.ihom.ev_naturality

added theorem CategoryTheory.ihom.ihom_adjunction_counit

added theorem CategoryTheory.ihom.ihom_adjunction_unit

added def CategoryTheory.ihom

added def CategoryTheory.tensorClosed

added def CategoryTheory.unitClosed