Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-13 22:32 27982536

View on Github →

Revert "feat(ring_theory/power_series): X s commutes with any power series" This reverts commit f1adf6ad90b09ebecc1d9ce1a11de81a839a4515.

Estimated changes

Modified src/ring_theory/power_series/basic.lean

deleted theorem mv_power_series.commute_X

deleted theorem mv_power_series.commute_monomial

deleted theorem power_series.commute_X

modified theorem power_series.order_eq_multiplicity_X