mathlib3
07a2c0d8 - doc(order/filter/zero_and_bounded_at_filter): tinker with docstrings (#16874)

Commit
3 years ago
doc(order/filter/zero_and_bounded_at_filter): tinker with docstrings (#16874) I found them a bit hard to understand.
Author
Parents
Loading