Commit 2022-01-08 15:04 43041277
View on Github →feat(ring_theory/power_series): teach simp to simplify more coercions of polynomials to power series (#11287)
So that simp can prove that the polynomial 5 * X^2 + X + 1 coerced to a power series is the same thing with the power series generator X. Likewise for mv_power_series.