Def CategoryTheory.Equivalence.Mon_.equivLaxMonoidalFunctorPUnit

Modification history

2025-07-28 06:06

Mathlib/CategoryTheory/Monoidal/Mon_.lean

chore(CategoryTheory/Monoidal): unify `mkIso` (#27126) …

Modified CategoryTheory.Equivalence.Mon_.equivLaxMonoidalFunctorPUnit View on Github →

2025-05-09 20:40

Mathlib/CategoryTheory/Monoidal/Mon_.lean

feat: an equivalence of categories lifts to an equivalence of their group objects (#23912) …

Added CategoryTheory.Equivalence.Mon_.equivLaxMonoidalFunctorPUnit View on Github →