Commit 2024-04-30 04:24 35c984e2
View on Github →chore: HahnSeries.ofPowerSeries_X_pow linter complains on nightly-testing (#12529)
On nightly-testing ofPowerSeries_X_pow becomes a bad simp lemma, because the LHS will simplify. Fix this by adding the missing lemma so the whole proof is just by simp, and remove @[simp].