Commit 2024-03-23 19:58 87ee74b1

View on Github →

fix: use binary recursion for Sum.pow (#11558) fixes #11543

Estimated changes

Modified Mathlib/Tactic/Linarith/Parsing.lean

deleted def Linarith.Sum.pow

Modified test/linarith.lean