Commit 2023-03-10 09:02 64a06a08

View on Github →

feat: port CategoryTheory.Monoidal.End (#2759)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/End.lean

added theorem CategoryTheory.associativity_app

added def CategoryTheory.endofunctorMonoidalCategory

added theorem CategoryTheory.left_unitality_app

added theorem CategoryTheory.obj_zero_map_μ_app

added theorem CategoryTheory.obj_ε_app

added theorem CategoryTheory.obj_ε_inv_app

added theorem CategoryTheory.obj_μ_app

added theorem CategoryTheory.obj_μ_inv_app

added theorem CategoryTheory.obj_μ_zero_app

added theorem CategoryTheory.right_unitality_app

added def CategoryTheory.tensoringRightMonoidal

added theorem CategoryTheory.ε_app_obj

added theorem CategoryTheory.ε_hom_inv_app

added theorem CategoryTheory.ε_inv_app_obj

added theorem CategoryTheory.ε_inv_hom_app

added theorem CategoryTheory.ε_inv_naturality

added theorem CategoryTheory.ε_naturality

added theorem CategoryTheory.μ_hom_inv_app

added theorem CategoryTheory.μ_inv_hom_app

added theorem CategoryTheory.μ_inv_naturality

added theorem CategoryTheory.μ_inv_naturalityᵣ

added theorem CategoryTheory.μ_inv_naturalityₗ

added theorem CategoryTheory.μ_naturality

added theorem CategoryTheory.μ_naturalityᵣ

added theorem CategoryTheory.μ_naturality₂

added theorem CategoryTheory.μ_naturalityₗ