Commit 2025-05-04 19:39 9f1b91b2

View on Github →

chore: move BinaryFan.swap earlier (#24592) This is not very related to ChosenFiniteProducts. From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

added def CategoryTheory.Limits.BinaryFan.assoc

added def CategoryTheory.Limits.BinaryFan.assocInv

added theorem CategoryTheory.Limits.BinaryFan.assocInv_fst

added theorem CategoryTheory.Limits.BinaryFan.assocInv_snd

added theorem CategoryTheory.Limits.BinaryFan.assoc_fst

added theorem CategoryTheory.Limits.BinaryFan.assoc_snd

added def CategoryTheory.Limits.BinaryFan.braiding

added theorem CategoryTheory.Limits.BinaryFan.braiding_hom_fst

added theorem CategoryTheory.Limits.BinaryFan.braiding_hom_snd

added theorem CategoryTheory.Limits.BinaryFan.braiding_inv_fst

added theorem CategoryTheory.Limits.BinaryFan.braiding_inv_snd

added def CategoryTheory.Limits.BinaryFan.leftUnitor

added def CategoryTheory.Limits.BinaryFan.rightUnitor

added def CategoryTheory.Limits.BinaryFan.swap

added theorem CategoryTheory.Limits.BinaryFan.swap_fst

added theorem CategoryTheory.Limits.BinaryFan.swap_snd

added theorem CategoryTheory.Limits.HasBinaryProduct.swap

added def CategoryTheory.Limits.IsLimit.binaryFanSwap

Modified Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean

deleted def CategoryTheory.Limits.BinaryFan.assoc

deleted def CategoryTheory.Limits.BinaryFan.assocInv

deleted theorem CategoryTheory.Limits.BinaryFan.assocInv_fst

deleted theorem CategoryTheory.Limits.BinaryFan.assocInv_snd

deleted theorem CategoryTheory.Limits.BinaryFan.assoc_fst

deleted theorem CategoryTheory.Limits.BinaryFan.assoc_snd

deleted def CategoryTheory.Limits.BinaryFan.braiding

deleted theorem CategoryTheory.Limits.BinaryFan.braiding_hom_fst

deleted theorem CategoryTheory.Limits.BinaryFan.braiding_hom_snd

deleted theorem CategoryTheory.Limits.BinaryFan.braiding_inv_fst

deleted theorem CategoryTheory.Limits.BinaryFan.braiding_inv_snd

deleted def CategoryTheory.Limits.BinaryFan.leftUnitor

deleted def CategoryTheory.Limits.BinaryFan.rightUnitor

deleted def CategoryTheory.Limits.BinaryFan.swap

deleted theorem CategoryTheory.Limits.BinaryFan.swap_fst

deleted theorem CategoryTheory.Limits.BinaryFan.swap_snd

deleted theorem CategoryTheory.Limits.HasBinaryProduct.swap

deleted def CategoryTheory.Limits.IsLimit.assoc

deleted def CategoryTheory.Limits.IsLimit.swapBinaryFan