Commit 2024-06-09 23:30 9f2d0a11
View on Github →feat(CategoryTheory/GradedObject): the triangle equality (#11687)
In this PR, we obtain the lemma GradedObject.mapBifunctor_triangle which promotes a triangle identity involving functors to a triangle identity for the induced functors on graded objects. More simp lemmas for isomorphisms like Iso.map_hom_inv_id_eval_app are also added in order to ease automation.