mathlib

eba9be51 - feat(ring_theory/power_series/basic): remove const coeff (#6383)

feat(ring_theory/power_series/basic): remove const coeff (#6383) This shows that we can factor out X when the constant coefficient is removed from a power series. Co-authored-by: Moritz Firsching <firsching@google.com>