Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2023-07-12 15:28
92bd7b1f
View on Github →
feat(analysis/convex): convexity of n-ary sums (
#18943
)
Estimated changes
Modified
src/analysis/convex/basic.lean
added
theorem
coe_convex_add_submonoid
added
def
convex_add_submonoid
added
theorem
convex_list_sum
added
theorem
convex_multiset_sum
added
theorem
convex_sum
added
theorem
convex_zero
added
theorem
mem_convex_add_submonoid
Modified
src/analysis/convex/combination.lean
added
def
convex_hull_add_monoid_hom
added
theorem
convex_hull_list_sum
added
theorem
convex_hull_multiset_sum
added
theorem
convex_hull_sum
Modified
src/analysis/convex/hull.lean
added
theorem
convex_hull_zero
Modified
src/measure_theory/measure/haar/of_basis.lean