mathlib
98061d12 - fix(tactic/linarith): treat powers like multiplication (#4082)

Commit
5 years ago
fix(tactic/linarith): treat powers like multiplication (#4082) `ring` understands that natural number exponents are repeated multiplication, so it's safe for `linarith` to do the same. This is unlikely to affect anything except `nlinarith` calls, which are now slightly more powerful. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Author
Parents
Loading