Mathlib v3 is deprecated. Go to Mathlib v4

Def Mon_.id

Modification history

2020-07-28 15:30

src/category_theory/monoidal/internal.lean

feat(category_theory): Mon_ (Type u) ≌ Mon.{u} (#3562) …

Added Mon_.id View on Github →