Commit 2023-10-20 06:54 afc57034

feat: add exponentiation option back to linear_combination (#7789) [mathlib3#15428](https://github.com/leanprover-community/mathlib/pull/15428) added an exponent option to linear_combination. The idea is that linear_combination (exp := 2) ... will take a linear combination of hypotheses adding up to the square of the goal. This is only mildly useful on its own, but it's a very useful certificate syntax for [mathlib3#15425](https://github.com/leanprover-community/mathlib/pull/15425).