Mathlib Changelog
Changelog
About
Github
Commit
2023-05-18 17:57
95a87616
View on Github →
chore(category_theory/monoidal/types): split file (
#19035
)
Estimated changes
Modified
src/algebra/category/Module/adjunctions.lean
Modified
src/category_theory/enriched/basic.lean
Modified
src/category_theory/monoidal/internal/types.lean
Renamed
src/category_theory/monoidal/of_chosen_finite_products.lean
to
src/category_theory/monoidal/of_chosen_finite_products/basic.lean
deleted
theorem
category_theory.monoidal_of_chosen_finite_products.braiding_naturality
deleted
theorem
category_theory.monoidal_of_chosen_finite_products.hexagon_forward
deleted
theorem
category_theory.monoidal_of_chosen_finite_products.hexagon_reverse
deleted
theorem
category_theory.monoidal_of_chosen_finite_products.symmetry
deleted
def
category_theory.symmetric_of_chosen_finite_products
Created
src/category_theory/monoidal/of_chosen_finite_products/symmetric.lean
added
theorem
category_theory.monoidal_of_chosen_finite_products.braiding_naturality
added
theorem
category_theory.monoidal_of_chosen_finite_products.hexagon_forward
added
theorem
category_theory.monoidal_of_chosen_finite_products.hexagon_reverse
added
theorem
category_theory.monoidal_of_chosen_finite_products.symmetry
added
def
category_theory.symmetric_of_chosen_finite_products
Renamed
src/category_theory/monoidal/types.lean
to
src/category_theory/monoidal/types/basic.lean
deleted
theorem
category_theory.braiding_hom_apply
deleted
theorem
category_theory.braiding_inv_apply
deleted
def
category_theory.coyoneda_tensor_unit
Created
src/category_theory/monoidal/types/coyoneda.lean
added
def
category_theory.coyoneda_tensor_unit
Created
src/category_theory/monoidal/types/symmetric.lean
added
theorem
category_theory.braiding_hom_apply
added
theorem
category_theory.braiding_inv_apply
Modified
src/representation_theory/Action.lean