mathlib

d44692a8 - refactor(analysis/convex/cone): move cone.lean to cone/basic.lean (#16270)

refactor(analysis/convex/cone): move cone.lean to cone/basic.lean (#16270) Part of #16266 I intend to create another file for `proper_cone`, which for cyclic import reasons cannot be included in cone.lean. So I want to move cone.lean to cone/basic.lean and create cone/proper.lean in a separate PR.