Commit 2022-09-21 10:15 aae2a82f

View on Github →

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.

Estimated changes