Commit 2023-05-25 08:46 e7e38679
View on Github →feat: assorted positivity extensions (#3907)
Positivity extensions for NonnegHomClass (this includes AbsoluteValue and Seminorm), IsAbsoluteValue, norm, the NNReal-to-Real coercion, factorials, square roots, distance (in a metric space), and diameter.
I tried to do these "properly" using Qq but I hit various errors I couldn't fix -- see
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Qq.20doesn't.20know.20that.20two.20things.20have.20the.20same.20type
for some examples.
cc @dwrensha