Def CommGrp_.mkIso'

Modification history

2025-10-16 01:23
Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
chore: rename `Grp_` to `Grp` (#30496) …
Deleted CommGrp_.mkIso'View on Github →
2025-09-14 15:36
Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
chore: rename `Mod_Class` to `ModObj` (#29641) …
Modified CommGrp_.mkIso'View on Github →
2025-09-14 10:28
Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
chore: rename `Grp_Class` to `GrpObj` (#29623) …
Modified CommGrp_.mkIso'View on Github →
2025-07-28 06:06
Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
chore(CategoryTheory/Monoidal): unify `mkIso` (#27126) …
Added CommGrp_.mkIso'View on Github →