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.

Estimated changes