Commit 2021-10-01 23:08 06b184f9

View on Github →

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

Estimated changes

Modified src/analysis/convex/caratheodory.lean

modified theorem eq_pos_convex_span_of_mem_convex_hull

Modified src/analysis/convex/extreme.lean

Modified src/analysis/convex/independent.lean

modified theorem convex_independent_iff_finset