Def Grp_.mkIso

Modification history

2025-07-28 06:06

Mathlib/CategoryTheory/Monoidal/Grp_.lean

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

Deleted Grp_.mkIso View on Github →

2025-02-09 16:53

Mathlib/CategoryTheory/Monoidal/Grp_.lean

feat(CategoryTheory): group objects (#21347) …

Added Grp_.mkIso View on Github →