Commit 2025-04-16 15:35 583dd351

View on Github →

feat (RingTheory/PowerSeries/Order) : compute order of power and generalize (#23993)

compute order of power of power series
generalize order_mul
generalize lemmas at the end to [Semiring R] [NoZeroDivisors R] by proving (PowerSeries.X_pow_mul_cancel) that one can divide out by powers on X on both sides of an equality.

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

added theorem trichotomy_of_mul_eq_mul

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem PowerSeries.X_mul_cancel

added theorem PowerSeries.X_mul_inj

added theorem PowerSeries.X_mul_pow_inj

added theorem PowerSeries.X_pow_mul_cancel

added theorem PowerSeries.commute_X_pow

deleted theorem PowerSeries.eq_zero_or_eq_zero_of_mul_eq_zero

added theorem PowerSeries.mul_X_cancel

added theorem PowerSeries.mul_X_inj

added theorem PowerSeries.mul_X_pow_cancel

added theorem PowerSeries.mul_X_pow_inj

Modified Mathlib/RingTheory/PowerSeries/Order.lean

modified theorem PowerSeries.divided_by_X_pow_order_of_X_eq_one

added theorem PowerSeries.le_order_pow

added theorem PowerSeries.order_pow