Commit 2025-04-21 18:16 32998106

View on Github →

chore(CategoryTheory/Whiskering): more lemmas about isoWhisker (#24252) Duplicate some of the whiskerLeft/whiskerRight lemmas for isoWhiskerLeft/isoWhiskerRight.

Estimated changes

Modified Mathlib/CategoryTheory/Whiskering.lean

added theorem CategoryTheory.Functor.pentagonIso

added theorem CategoryTheory.Functor.triangleIso

added theorem CategoryTheory.isoWhiskerLeft_refl

added theorem CategoryTheory.isoWhiskerLeft_right

added theorem CategoryTheory.isoWhiskerLeft_symm

added theorem CategoryTheory.isoWhiskerLeft_trans

added theorem CategoryTheory.isoWhiskerLeft_trans_isoWhiskerRight

added theorem CategoryTheory.isoWhiskerLeft_twice

added theorem CategoryTheory.isoWhiskerRight_left

added theorem CategoryTheory.isoWhiskerRight_refl

added theorem CategoryTheory.isoWhiskerRight_symm

added theorem CategoryTheory.isoWhiskerRight_trans

added theorem CategoryTheory.isoWhiskerRight_twice