mathlib

4a927b25 - feat(algebra/order/hom/monoid): add `monotone_iff_map_nonneg/pos` + golf (#16601)

feat(algebra/order/hom/monoid): add `monotone_iff_map_nonneg/pos` + golf (#16601) If the source is an ordered add_group, a monoid hom is monotone if and only if it sends nonnegative elements to a nonnegative elements. This connects the notion of [positive linear functional](https://en.wikipedia.org/wiki/Positive_linear_functional) to monotonicity. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Amenable.20Groups/near/300076886)