Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-02-26 23:59
cda31e7e
View on Github →
refactor(CategoryTheory/Monoidal/Rigid): use monoidalComp in the proofs (
#10326
) Similar to
#10078
Estimated changes
Modified
Mathlib/CategoryTheory/Monoidal/Functor.lean
added
theorem
CategoryTheory.MonoidalFunctor.map_whiskerLeft'
added
theorem
CategoryTheory.MonoidalFunctor.map_whiskerRight'
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
added
theorem
CategoryTheory.ExactPairing.coevaluation_evaluation''
added
theorem
CategoryTheory.ExactPairing.evaluation_coevaluation''
deleted
theorem
CategoryTheory.tensorLeftHomEquiv_id_tensor_comp_evaluation
deleted
theorem
CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_id_tensor
deleted
theorem
CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_tensor_id
added
theorem
CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft
added
theorem
CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight
deleted
theorem
CategoryTheory.tensorLeftHomEquiv_tensor_id_comp_evaluation
added
theorem
CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluation
added
theorem
CategoryTheory.tensorLeftHomEquiv_whiskerRight_comp_evaluation
deleted
theorem
CategoryTheory.tensorRightHomEquiv_id_tensor_comp_evaluation
deleted
theorem
CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_id_tensor
deleted
theorem
CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_tensor_id
added
theorem
CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft
added
theorem
CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight
deleted
theorem
CategoryTheory.tensorRightHomEquiv_tensor_id_comp_evaluation
added
theorem
CategoryTheory.tensorRightHomEquiv_whiskerLeft_comp_evaluation
added
theorem
CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_evaluation
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean
Modified
Mathlib/Tactic/CategoryTheory/Coherence.lean