Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi.default_def

Modification history

2022-06-20 13:49
src/logic/unique.lean
feat(logic/unique): functions from a `unique` type is `const` (#14823) …
Modified pi.default_defView on Github →
2020-10-08 15:41
src/logic/unique.lean
chore(*): add a few more `unique` instances (#4511) …
Added pi.default_defView on Github →