Commit 2020-10-30 08:20 63c0dac6

View on Github →

refactor(module/ordered): make ordered_semimodule a mixin (#4719) Per @urkud's suggestion at #4683. This should avoid having to introduce a separate ordered_algebra class.

Estimated changes

Modified src/algebra/module/ordered.lean

added theorem ordered_semimodule.mk''

deleted def ordered_semimodule.mk''

added theorem ordered_semimodule.mk'

deleted def ordered_semimodule.mk'

Modified src/analysis/convex/basic.lean

modified theorem concave_on.concave_le

modified theorem concave_on.convex_hypograph

modified theorem concave_on.convex_lt

modified theorem concave_on.smul

modified theorem concave_on_iff_convex_hypograph

modified theorem convex_on.convex_epigraph

modified theorem convex_on.convex_le

modified theorem convex_on.convex_lt

modified theorem convex_on.smul

modified theorem convex_on_iff_convex_epigraph

modified theorem neg_concave_on_iff

modified theorem neg_convex_on_iff

Modified src/analysis/convex/cone.lean

added theorem convex_cone.to_ordered_semimodule

deleted def convex_cone.to_ordered_semimodule

Modified src/analysis/convex/extrema.lean

Modified src/linear_algebra/affine_space/ordered.lean