Def CategoryTheory.uliftTrivial

Modification history

2023-02-28 20:37
Mathlib/CategoryTheory/Types.lean
feat: add to_additive linter checking whether additive decl exists (#1881) …
Modified CategoryTheory.uliftTrivialView on Github →
2023-02-15 17:16
Mathlib/CategoryTheory/Types.lean
feat: port CategoryTheory.Types (#2294)
Added CategoryTheory.uliftTrivialView on Github →