Commit 2021-04-27 07:21 287492c6

View on Github →

refactor(ring_theory/hahn_series): non-linearly-ordered Hahn series (#7377) Refactors Hahn series to use set.is_pwo instead of set.is_wf, allowing them to be defined on non-linearly-ordered monomial types

Estimated changes

Modified src/order/well_founded_set.lean

modified theorem finset.is_pwo

added theorem finset.is_pwo_sup

added theorem finset.is_pwo_support_mul_antidiagonal

modified theorem finset.is_wf

deleted theorem finset.is_wf_support_mul_antidiagonal

modified theorem finset.mul_antidiagonal_min_mul_min

modified theorem finset.partially_well_ordered_on

modified theorem finset.well_founded_on

added theorem set.finite.is_pwo

deleted theorem set.finite.is_wf

added theorem set.fintype.is_pwo

deleted theorem set.fintype.is_wf

added theorem set.is_pwo.insert

modified theorem set.is_pwo.mul

added theorem set.is_pwo.union

added theorem set.is_pwo_empty

added theorem set.is_pwo_singleton

deleted theorem set.is_wf.insert

deleted theorem set.is_wf_empty

deleted theorem set.is_wf_singleton

added theorem set.partially_well_ordered_on.mono

Modified src/ring_theory/hahn_series.lean

added theorem hahn_series.is_pwo_support

modified theorem hahn_series.is_wf_support

modified theorem hahn_series.mul_coeff_left'

modified theorem hahn_series.mul_coeff_min_add_min

modified theorem hahn_series.mul_coeff_right'

added theorem hahn_series.summable_family.is_pwo_Union_support

deleted theorem hahn_series.summable_family.is_wf_Union_support

modified structure hahn_series