mathlib
c5e83e00
- chore(analysis/convex/cone): set_like instance (#15715)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(analysis/convex/cone): set_like instance (#15715) This removes lots of lemmas that are already in the `set_like` namespace. `convex_cone.ext'` is now `set_like.coe_injective`.
Author
eric-wieser
Parents
dd6f53d8
Loading