Def Polynomial.toPowerSeries

Modification history

2024-10-27 12:33

Mathlib/RingTheory/PowerSeries/Basic.lean

chore(RingTheory/PowerSeries/Basic): rename `Polynomial.ToPowerSeries` -> `Polynomial.toPowerSeries` (#18265) …

Added Polynomial.toPowerSeries View on Github →