Theorem Grp_.id'

Modification history

2025-10-16 01:23
Mathlib/CategoryTheory/Monoidal/Grp_.lean
chore: rename `Grp_` to `Grp` (#30496) …
Deleted Grp_.id'View on Github →
2025-09-17 06:03
Mathlib/CategoryTheory/Monoidal/Grp_.lean
chore: rename `Mon_`, `Comon_`, ... to `Mon`, `Comon`, etc (#29660) …
Modified Grp_.id'View on Github →
2025-02-09 16:53
Mathlib/CategoryTheory/Monoidal/Grp_.lean
feat(CategoryTheory): group objects (#21347) …
Added Grp_.id'View on Github →