Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eq_const_of_unique

Modification history

2022-06-20 13:49

src/logic/unique.lean

feat(logic/unique): functions from a `unique` type is `const` (#14823) …

Added eq_const_of_unique View on Github →