Commit 2026-01-31 09:49 fbc09fe0
View on Github →feat(NumberTheory/Height/Basic): positivity extensions (#34534)
This PR adds extensions for the positivity tactic so that it knows that Height.mulHeight₁ x and Height.mulHeight x are positive and Height.logHeight₁ x and Height.logHeight are nonnegative.