Mathlib v3 is deprecated. Go to Mathlib v4

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