Commit 2021-01-07 10:05 2c8175fa

View on Github →

feat(algebra/algebra/ordered): ordered algebras (#4683) An ordered algebra is an ordered semiring, which is an algebra over an ordered commutative semiring, for which scalar multiplication is "compatible" with the two orders.

Estimated changes

Created src/algebra/algebra/ordered.lean

added theorem algebra_map_monotone

Modified src/algebra/ordered_ring.lean

Modified src/analysis/convex/basic.lean

modified theorem concave_on.subset

modified theorem convex.mem_Icc