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.

Estimated changes