Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi.default_apply

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_apply View on Github →

2020-10-08 15:41

src/logic/unique.lean

chore(*): add a few more `unique` instances (#4511) …

Added pi.default_apply View on Github →