Commit 2025-04-03 18:22 10a49d76

View on Github →

chore(CategoryTheory/Whiskering): lemmas about NatTrans.hcomp and whiskering (#23639) Add basic lemmas that were missing in the API.

Estimated changes

Modified Mathlib/CategoryTheory/Whiskering.lean

added theorem CategoryTheory.NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight

added theorem CategoryTheory.NatTrans.hcomp_id

added theorem CategoryTheory.NatTrans.id_hcomp

added theorem CategoryTheory.whiskerLeft_comp_whiskerRight