Commit 2022-12-13 22:30 f1adf6ad
View on Github →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?