mathlib3
e51377fe - feat(logic/basic): `ulift.down` is injective (#12824)

Commit

3 years ago

feat(logic/basic): `ulift.down` is injective (#12824) We also make the arguments to `plift.down_inj` inferred.

Author

vihdzp

Parents