mathlib3

f1adf6ad - feat(ring_theory/power_series): `X s` commutes with any power series

feat(ring_theory/power_series): `X s` commutes with any power series 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?