Def Mon_.mkIso

Modification history

2025-07-28 06:06

Mathlib/CategoryTheory/Monoidal/Mon_.lean

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

Deleted Mon_.mkIso View on Github →

2025-06-04 18:15

Mathlib/CategoryTheory/Monoidal/Mon_.lean

feat(CategoryTheory/Monoidal): define Mon_ by using Mon_Class (#24646) …

Modified Mon_.mkIso View on Github →

2024-06-01 00:00

Mathlib/CategoryTheory/Monoidal/Mon_.lean

feat(CategoryTheory/Monoidal/Bimon): definition of bimonoid object in a braided category (#12970)

Added Mon_.mkIso View on Github →