mathlib3

aae2a82f - feat(algebra/order/hom/basic): `positivity` extension for nonnegative homs (#16228)

feat(algebra/order/hom/basic): `positivity` extension for nonnegative homs (#16228) Add `positivity_map`, a `positivity` extension for expressions of the form `f x` where `f : F` where `nonneg_hom_class F α β`. Golf existing proofs using it.