Commit 2021-03-14 00:42 1b0db8e3

View on Github →

feat(order/well_founded_set, ring_theory/hahn_series): hahn_series.add_val (#6564) Defines set.is_wf.min in terms of well_founded.min Places an add_valuation, hahn_series.add_val, on hahn_series

Estimated changes

Modified src/order/well_founded_set.lean

added theorem finset.mul_antidiagonal_min_mul_min

added theorem set.is_wf.le_min_iff

added theorem set.is_wf.min_le

added theorem set.is_wf.min_le_min_of_subset

added theorem set.is_wf.min_mem

added theorem set.is_wf.min_mul

added theorem set.is_wf.min_union

added theorem set.is_wf.not_lt_min

added theorem set.is_wf_min_singleton

Modified src/ring_theory/hahn_series.lean

added def hahn_series.add_val

added theorem hahn_series.add_val_apply

added theorem hahn_series.add_val_apply_of_ne

added theorem hahn_series.coeff_min_ne_zero

added theorem hahn_series.mul_coeff_min_add_min

modified theorem hahn_series.single_coeff_same

added theorem hahn_series.support_add_subset

added theorem hahn_series.support_nonempty_iff

added theorem hahn_series.support_one