mathlib3

7d6cd041 - feat(ring_theory/power_series): `X s` commutes with any power series (#17935)

feat(ring_theory/power_series): `X s` commutes with any power series (#17935) Use this fact to golf a proof and generalize `order_eq_multiplicity_X` from `[comm_semiring R]` to `[semiring R]`. Should we redefine `order` to be `multiplicity` in all cases?