Commit 2021-10-05 08:05 fefd8a38
View on Github →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.