mathlib

915591b2 - chore(analysis/convex/cone/basic): split (#19043)

chore(analysis/convex/cone/basic): split (#19043) Split out the inner product space material (the dual cone) from `analysis/convex/cone/basic`. What's left imports almost nothing, and can probably be ported immediately.