Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ulift.rec.constant

Modification history

2021-08-26 11:17
src/control/ulift.lean
refactor(*): move code about `ulift`/`plift` (#8863) …
Modified ulift.rec.constantView on Github →
2020-07-29 11:19
src/data/ulift.lean
feat(data/ulift): add `monad ulift` and `monad plift` (#3588) …
Modified ulift.rec.constantView on Github →
2020-06-02 00:43
src/data/ulift.lean
chore(*): split long lines (#2913)
Modified ulift.rec.constantView on Github →
2018-12-20 23:12
data/ulift.lean
feat(category_theory): assorted small changes from the old limits PR (#512)
Added ulift.rec.constantView on Github →