Theorem eq_pos_convex_span_of_mem_convex_hull
Modification history
2021-10-01 23:08
src/analysis/convex/caratheodory.lean
refactor(analysis/convex/caratheodory): generalize ℝ to an arbitrary linearly ordered field (#9479) …
Modified eq_pos_convex_span_of_mem_convex_hullView on Github →