Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-08-17 15:28
d4cb2372
View on Github →
feat(algebra/module): define ordered semimodules and generalize convexity of functions (
#3728
)
Estimated changes
Created
src/algebra/module/ordered.lean
added
theorem
smul_le_smul_of_nonneg
added
theorem
smul_lt_smul_of_pos
Modified
src/analysis/convex/basic.lean
modified
theorem
convex_on.add
modified
theorem
convex_on.comp_affine_map
modified
theorem
convex_on.comp_linear_map
modified
theorem
convex_on.convex_epigraph
modified
theorem
convex_on.convex_le
modified
theorem
convex_on.convex_lt
modified
theorem
convex_on.le_on_segment'
modified
theorem
convex_on.le_on_segment
modified
theorem
convex_on.smul
modified
theorem
convex_on.subset
modified
theorem
convex_on.translate_left
modified
theorem
convex_on.translate_right
modified
def
convex_on
modified
theorem
convex_on_const
modified
theorem
convex_on_iff_convex_epigraph
deleted
theorem
convex_on_iff_div:
added
theorem
convex_on_iff_div
modified
theorem
linear_order.convex_on_of_lt
Modified
src/analysis/convex/specific_functions.lean
modified
theorem
convex_on_fpow
modified
theorem
convex_on_pow
modified
theorem
convex_on_pow_of_even
modified
theorem
convex_on_rpow