Mathlib v3 is deprecated. Go to Mathlib v4

Theorem unique.default_eq

Modification history

2022-01-09 18:06
src/logic/unique.lean
chore(*): update to 3.37.0c (#11325) …
Modified unique.default_eqView on Github →
2019-01-18 19:50
src/logic/unique.lean
feat(logic/basic): add class 'unique' for uniquely inhabited types (#605)
Added unique.default_eqView on Github →