!3#18779

Stream: PR reviews

[Jireh Loreaux]

because of the concensus on !3#18230 (see https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/!3.2318230.20Positivity.20of.20linear.20maps), and the fact that this PR depends on that one in an essential way, I am removing the not-too-late tag on this PR. However, I'm not closing it for the same reason as !3#18230, so that it serves as a reminder that we don't have this in mathlib yet, but that we want to go about it a different way.