Commit 2024-07-11 17:04 8a1d23ab

View on Github →

feat: Product of convex hulls (#13952) From LeanCamCombi

Estimated changes

Modified Mathlib/Algebra/BigOperators/Ring.lean

added theorem Fintype.prod_sum

Modified Mathlib/Algebra/Module/BigOperators.lean

modified theorem Finset.sum_smul_sum

added theorem Fintype.sum_smul_sum

Modified Mathlib/Analysis/Convex/Combination.lean

added theorem convexHull_pi

added theorem mem_convexHull_iff_exists_fintype

added theorem mem_convexHull_of_exists_fintype

added theorem mem_convexHull_pi

Modified Mathlib/Analysis/Convex/Hull.lean

modified theorem convexHull_neg

modified theorem convexHull_smul

added theorem convexHull_vadd

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean