Def Grp_.forget

Modification history

2025-08-30 20:09

Mathlib/CategoryTheory/Monoidal/Grp_.lean

feat: tensor product of group objects (#29134) …

Deleted Grp_.forget View on Github →

2025-02-09 16:53

Mathlib/CategoryTheory/Monoidal/Grp_.lean

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

Added Grp_.forget View on Github →