caratheodory): generalize ℝ to an arbitrary linearly ordered field (#9479)

Commit

4 years ago

refactor(analysis/convex/caratheodory): generalize ℝ to an arbitrary linearly ordered field (#9479) As a result; `convex_independent_iff_finset` also gets generalized.

Author

YaelDillies

Parents

118d45ad

mathlib 06b184f9 - refactor(analysis/convex/caratheodory): generalize ℝ to an arbitrary linearly ordered field (#9479)

mathlib
06b184f9 - refactor(analysis/convex/caratheodory): generalize ℝ to an arbitrary linearly ordered field (#9479)