MulPosMono

Stream: mathlib4

[Kevin Buzzard]

Why is docs#MulPosMono not called MulNonnegMono?

[Matthew Ballard]

I clicked on it and spent a few seconds wondering why it was a monomorphism

[Damiano Testa]

I think that the reason is mostly historical: in my initial draft, I was not sure whether I wanted to have multiplication by positive or non-negative elements, so I made a choice. Then the choice changed, but the name stayed.

On a side note, after the PR got merged, I belatedly agreed with Floris that the abbreviation was probably not necessarily an improvement over using the explicit CovariantClass name. But also not worth going back and removing it.