Def CategoryTheory.Grp.trivial

Modification history

2026-05-08 08:38
Mathlib/CategoryTheory/Monoidal/Grp.lean
chore(*): small fixes for `backward.inferInstanceAs` tech debt (#39012) …
Modified CategoryTheory.Grp.trivialView on Github →
2025-10-30 04:20
Mathlib/CategoryTheory/Monoidal/Grp_.lean
chore(CategoryTheory): namespace `Mon`, `Grp`, etc... (#30786) …
Added CategoryTheory.Grp.trivialView on Github →