Commit 2023-01-05 19:47 19e17ae2
View on Github →feat: add Inv, Abs, and natAbs positivity extensions (#1190)
Adds positivity
extensions for inversion, absolute value, and natAbs.
Compare the the mathlib3 versions here, here, and here.
For the absolute value case, I got stuck trying to make it work in the fully Qq
-ified style, so I fell back to the AppBuilder
style that's closer to how mathlib3 does it.