Commit 2023-12-17 21:55 7b1f933b

feat: positivity extension for zpow (#8003) This PR adds a positivity extension for integer powers, i.e. a ^ (r : ℤ). It's basically copy-pasted from the natural power extension. Note that this makes the imports of Mathlib.Tactic.Positivity.Basic slightly heavier since the required lemmas were not there (and the relevant file doesn't import positivity so I couldn't put it there either). It's probably not too bad, but I can put it in a new file if people think this would be better.