Commit 2024-11-22 18:05 178af37e
View on Github →feat(RingTheory/PowerSeries/Basic): Polynomial.coe_sub and Polynomial.coe_neg (#19339)
These are analogous to the existing Polynomial.coe_add and Polynomial.coe_zero, about the coercion from Polynomial to PowerSeries.
Zulip thread.