Commit 2022-12-14 17:12 7d6cd041
View on Github →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?