mathlib
9f33b7dd - feat(algebra/ordered_*): arithmetic operations on monotone functions (#2634)

Commit

6 years ago

feat(algebra/ordered_*): arithmetic operations on monotone functions (#2634) Also move `strict_mono` to `order/basic` and add a module docstring.

References

Author

urkud

Parents