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]
.