Commit 2025-05-16 00:53 c4a97f5f

View on Github →

chore: avoid Coe.coe in PowerSeries (#24887)

Estimated changes

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

modified theorem Polynomial.coe_injective

modified def Polynomial.toPowerSeries