Commit 2022-07-27 17:03 c59720b4
View on Github →chore(analysis/convex/cone): add trivial coercion lemmas (#15713)
This also changes le to unfold in terms of coe rather than carrier, since that's the form we have lemmas about.
chore(analysis/convex/cone): add trivial coercion lemmas (#15713)
This also changes le to unfold in terms of coe rather than carrier, since that's the form we have lemmas about.