Mathlib v3 is deprecated. Go to Mathlib v4

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?

Estimated changes