Commit 2025-04-15 07:29 d730d225

View on Github →

chore(Analysis/Convex/Combination): remove open scoped Classical from theorems (#24057) These statements are more general with DecidableEq.

Estimated changes

Modified Mathlib/Analysis/Convex/Combination.lean

modified theorem AffineIndependent.convexHull_inter'

modified theorem Finset.centerMass_insert

modified theorem Finset.centerMass_ite_eq

modified theorem Finset.centerMass_pair

modified theorem convexHull_basis_eq_stdSimplex