Commit 2024-09-18 22:25 81fe23e7

View on Github →

feat(MvPowerSeries.LexOrder): lexicographic order of multivariate power series (#14981) Define the order of multivariate power series with respect to the lexicographic order on monomials. Prove that the ring of multivariate power series over a domain is a domain. Extension to some rings of Hahn series

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Basic.lean

added def LinearOrder.swap

Modified Mathlib/RingTheory/HahnSeries/PowerSeries.lean

Created Mathlib/RingTheory/MvPowerSeries/LexOrder.lean

added theorem MvPowerSeries.coeff_eq_zero_of_lt_lexOrder

added theorem MvPowerSeries.coeff_mul_of_add_lexOrder

added theorem MvPowerSeries.coeff_ne_zero_of_lexOrder

added theorem MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero

added theorem MvPowerSeries.le_lexOrder_iff

added theorem MvPowerSeries.le_lexOrder_mul

added theorem MvPowerSeries.lexOrder_def_of_ne_zero

added theorem MvPowerSeries.lexOrder_eq_top_iff_eq_zero

added theorem MvPowerSeries.lexOrder_le_of_coeff_ne_zero

added theorem MvPowerSeries.lexOrder_mul

added theorem MvPowerSeries.lexOrder_zero

added theorem MvPowerSeries.min_lexOrder_le

Modified Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean