Commit 2024-07-05 20:21 6adb24fe

View on Github →

feat (RingTheory/HahnSeries) : def leadingCoeff, orderTop lemmas (#12996) This PR defines a leadingCoeff function on Hahn series. For nonzero Hahn series, it returns the coefficient of the minimum element of support. For zero, it returns zero. This function generalizes x.coeff x.order to the setting where the exponent type does not have zero.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

added def HahnSeries.addOppositeEquiv

added theorem HahnSeries.addOppositeEquiv_leadingCoeff

added theorem HahnSeries.addOppositeEquiv_orderTop

added theorem HahnSeries.addOppositeEquiv_support

added theorem HahnSeries.addOppositeEquiv_symm_leadingCoeff

added theorem HahnSeries.addOppositeEquiv_symm_orderTop

added theorem HahnSeries.addOppositeEquiv_symm_support

added theorem HahnSeries.leadingCoeff_add_eq_left

added theorem HahnSeries.leadingCoeff_add_eq_right

added theorem HahnSeries.leadingCoeff_sub

added theorem HahnSeries.min_orderTop_le_orderTop_add

added theorem HahnSeries.min_orderTop_le_orderTop_sub

added theorem HahnSeries.orderTop_add_eq_left

added theorem HahnSeries.orderTop_add_eq_right

added theorem HahnSeries.orderTop_neg

added theorem HahnSeries.orderTop_sub

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

added def HahnSeries.leadingCoeff

added theorem HahnSeries.leadingCoeff_eq

added theorem HahnSeries.leadingCoeff_eq_iff

added theorem HahnSeries.leadingCoeff_ne_iff

added theorem HahnSeries.leadingCoeff_of_ne

added theorem HahnSeries.leadingCoeff_of_single

added theorem HahnSeries.leadingCoeff_zero

added theorem HahnSeries.lt_orderTop_single

added theorem HahnSeries.orderTop_single_le

added theorem HahnSeries.zero_le_orderTop_iff

added theorem HahnSeries.zero_lt_orderTop_iff

added theorem HahnSeries.zero_lt_orderTop_of_order