Theorem CategoryTheory.NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight

Modification history

2025-07-02 09:20

Mathlib/CategoryTheory/Whiskering.lean

chore(CategoryTheory): rename `whiskerLeft` to `Functor.whiskerLeft` (#26611) …

Deleted CategoryTheory.NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight View on Github →

2025-04-03 18:22

Mathlib/CategoryTheory/Whiskering.lean

chore(CategoryTheory/Whiskering): lemmas about `NatTrans.hcomp` and `whiskering` (#23639) …

Added CategoryTheory.NatTrans.hcomp_eq_whiskerLeft_comp_whiskerRight View on Github →