Commit 2025-04-16 20:00 422961d2

View on Github →

chore: cleanup API around order of univariate power series (#24072) The main changes are:

avoid ENat.lift in favor of ENat.toNat to avoid dependent types
change a bunch of order φ < ⊤ assumptions to φ ≠ 0
rename divided_by_X_pow_order to divXPowOrder, and define it concretely for any power series by translating the coefficients (meaning we send 0 to 0)
some golfs in the proofs

Estimated changes

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

added theorem MvPowerSeries.X_mul

added theorem MvPowerSeries.X_pow_mul

added theorem MvPowerSeries.commute_X_pow

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem PowerSeries.X_mul

added theorem PowerSeries.X_mul_injective

deleted theorem PowerSeries.X_mul_pow_inj

added theorem PowerSeries.X_pow_mul

added theorem PowerSeries.X_pow_mul_inj

added theorem PowerSeries.X_pow_mul_injective

modified theorem PowerSeries.commute_X_pow

added theorem PowerSeries.mul_X_injective

added theorem PowerSeries.mul_X_pow_injective

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean

Modified Mathlib/RingTheory/PowerSeries/Order.lean

modified theorem PowerSeries.X_pow_order_dvd

added theorem PowerSeries.X_pow_order_mul_divXPowOrder

added theorem PowerSeries.coe_toNat_order

added theorem PowerSeries.coeff_divXPowOrder

added theorem PowerSeries.coeff_of_lt_order_toNat

modified theorem PowerSeries.coeff_order

added theorem PowerSeries.constantCoeff_divXPowOrder

added theorem PowerSeries.constantCoeff_divXPowOrder_eq_zero_iff

added def PowerSeries.divXPowOrder

added theorem PowerSeries.divXPowOrder_X

added theorem PowerSeries.divXPowOrder_mul_divXPowOrder

added theorem PowerSeries.divXPowOrder_zero

deleted def PowerSeries.divided_by_X_pow_order

deleted theorem PowerSeries.divided_by_X_pow_orderMul

deleted theorem PowerSeries.divided_by_X_pow_order_of_X_eq_one

modified theorem PowerSeries.order_zero_of_unit

deleted theorem PowerSeries.self_eq_X_pow_order_mul_divided_by_X_pow_order