Theorem CategoryTheory.LaxBraidedFunctor.hom_ext

Modification history

2025-12-18 13:14
Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure (#26446) …
Modified CategoryTheory.LaxBraidedFunctor.hom_extView on Github →
2024-11-10 22:57
Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal (#17904) …
Added CategoryTheory.LaxBraidedFunctor.hom_extView on Github →