basic): generalize `concave_on.le_on_segment` to monoids (#8959)

Commit

4 years ago

chore(analysis/convex/basic): generalize `concave_on.le_on_segment` to monoids (#8959) This matches the generalization already present on `convex_on.le_on_segment`.

Author

pechersky

Parents

9d3e3e8a

mathlib3 8da6699f - chore(analysis/convex/basic): generalize `concave_on.le_on_segment` to monoids (#8959)

mathlib3
8da6699f - chore(analysis/convex/basic): generalize `concave_on.le_on_segment` to monoids (#8959)