Commit 2024-11-12 19:15 afafe9fd

View on Github →

feat(MvPowerSeries.Order): order of multivariate power series (#14983)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finsupp/Weight.lean

added theorem Finsupp.finite_of_degree_le

added theorem Finsupp.finite_of_nat_weight_le

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

added theorem MvPowerSeries.coeff_apply

added theorem MvPowerSeries.eq_zero_iff_forall_coeff_zero

added theorem MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero

Created Mathlib/RingTheory/MvPowerSeries/Order.lean

added theorem MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder

added theorem MvPowerSeries.coeff_homogeneousComponent

added theorem MvPowerSeries.coeff_mul_left_one_sub_of_lt_order

added theorem MvPowerSeries.coeff_mul_left_one_sub_of_lt_weightedOrder

added theorem MvPowerSeries.coeff_mul_prod_one_sub_of_lt_order

added theorem MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder

added theorem MvPowerSeries.coeff_mul_right_one_sub_of_lt_order

added theorem MvPowerSeries.coeff_mul_right_one_sub_of_lt_weightedOrder

added theorem MvPowerSeries.coeff_of_lt_order

added theorem MvPowerSeries.coeff_weightedHomogeneousComponent

added theorem MvPowerSeries.eq_zero_iff_forall_coeff_eq_zero_and

added theorem MvPowerSeries.exists_coeff_ne_zero_and_order

added theorem MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder

added def MvPowerSeries.homogeneousComponent

added theorem MvPowerSeries.le_order

added theorem MvPowerSeries.le_order_mul

added theorem MvPowerSeries.le_weightedOrder

added theorem MvPowerSeries.le_weightedOrder_mul

added theorem MvPowerSeries.min_order_le_add

added theorem MvPowerSeries.min_weightedOrder_le_add

added theorem MvPowerSeries.nat_le_order

added theorem MvPowerSeries.nat_le_weightedOrder

added theorem MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_degree

added theorem MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight

added theorem MvPowerSeries.ne_zero_iff_order_finite

added theorem MvPowerSeries.ne_zero_iff_weightedOrder_finite

added def MvPowerSeries.order

added theorem MvPowerSeries.order_add_of_order_ne

added theorem MvPowerSeries.order_eq_nat

added theorem MvPowerSeries.order_eq_top_iff

added theorem MvPowerSeries.order_le

added theorem MvPowerSeries.order_monomial

added theorem MvPowerSeries.order_monomial_of_ne_zero

added theorem MvPowerSeries.order_zero

added def MvPowerSeries.weightedHomogeneousComponent

added def MvPowerSeries.weightedOrder

added theorem MvPowerSeries.weightedOrder_add_of_weightedOrder_ne

added theorem MvPowerSeries.weightedOrder_eq_nat

added theorem MvPowerSeries.weightedOrder_eq_top_iff

added theorem MvPowerSeries.weightedOrder_le

added theorem MvPowerSeries.weightedOrder_monomial

added theorem MvPowerSeries.weightedOrder_monomial_of_ne_zero

added theorem MvPowerSeries.weightedOrder_zero

Modified Mathlib/RingTheory/PowerSeries/Order.lean

deleted theorem PowerSeries.le_order_add

added theorem PowerSeries.le_order_mul

added theorem PowerSeries.min_order_le_order_add

deleted theorem PowerSeries.order_mul_ge