Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-07-20 12:35
75d6f9e2
View on Github →
feat: missing definitional lemmas for the braiding on
Mon_ C
(
#27060
) From Toric
Estimated changes
Modified
Mathlib/CategoryTheory/Monoidal/Mon_.lean
added
theorem
CategoryTheory.Equivalence.Mon_.braiding_hom_hom
added
theorem
CategoryTheory.Equivalence.Mon_.braiding_inv_hom