Theorem CommMon_.mkIso_hom_hom

Modification history

2025-07-28 06:06
Mathlib/CategoryTheory/Monoidal/CommMon_.lean
chore(CategoryTheory/Monoidal): unify `mkIso` (#27126) …
Deleted CommMon_.mkIso_hom_homView on Github →
2024-11-10 22:57
Mathlib/CategoryTheory/Monoidal/CommMon_.lean
refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal (#17904) …
Added CommMon_.mkIso_hom_homView on Github →