mathlib

fefd8a38 - refactor(analysis/convex/*): prove `convex_independent_iff_finset` without full Carathéodory (#9550)

refactor(analysis/convex/*): prove `convex_independent_iff_finset` without full Carathéodory (#9550) Also relax one `add_comm_group` to `add_comm_monoid` and two `𝕜` to `β` + `module 𝕜 β`, and simplify imports.