Commit 2025-12-11 08:08 7d408fff

View on Github →

feat(CategoryTheory): commutation of bifunctors with shifts in two variables (#32303) This will be used when formalising triangulated bifunctors.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Center/NegOnePow.lean

added theorem CategoryTheory.CatCenter.app_neg_one_zpow

Created Mathlib/CategoryTheory/Shift/CommShiftTwo.lean

added structure CategoryTheory.CommShift₂Setup

Modified Mathlib/CategoryTheory/Shift/Twist.lean