Commit 2023-05-23 12:52 178cf0f7

View on Github →

feat: port RingTheory.HahnSeries (#4261)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

Created Mathlib/RingTheory/HahnSeries.lean

added def HahnSeries.C

added theorem HahnSeries.C_eq_algebraMap

added theorem HahnSeries.C_injective

added theorem HahnSeries.C_mul_eq_smul

added theorem HahnSeries.C_ne_zero

added theorem HahnSeries.C_one

added theorem HahnSeries.C_zero

added theorem HahnSeries.SummableFamily.add_apply

added theorem HahnSeries.SummableFamily.coe_add

added theorem HahnSeries.SummableFamily.coe_injective

added theorem HahnSeries.SummableFamily.coe_neg

added theorem HahnSeries.SummableFamily.coe_ofFinsupp

added theorem HahnSeries.SummableFamily.coe_powers

added theorem HahnSeries.SummableFamily.coe_sub

added theorem HahnSeries.SummableFamily.coe_zero

added def HahnSeries.SummableFamily.embDomain

added theorem HahnSeries.SummableFamily.embDomain_apply

added theorem HahnSeries.SummableFamily.embDomain_image

added theorem HahnSeries.SummableFamily.embDomain_notin_range

added theorem HahnSeries.SummableFamily.embDomain_succ_smul_powers

added theorem HahnSeries.SummableFamily.ext

added theorem HahnSeries.SummableFamily.finite_co_support

added def HahnSeries.SummableFamily.hsum

added theorem HahnSeries.SummableFamily.hsum_add

added theorem HahnSeries.SummableFamily.hsum_coeff

added theorem HahnSeries.SummableFamily.hsum_embDomain

added theorem HahnSeries.SummableFamily.hsum_ofFinsupp

added theorem HahnSeries.SummableFamily.hsum_smul

added theorem HahnSeries.SummableFamily.hsum_sub

added theorem HahnSeries.SummableFamily.isPwo_iUnion_support

added def HahnSeries.SummableFamily.lsum

added theorem HahnSeries.SummableFamily.neg_apply

added def HahnSeries.SummableFamily.ofFinsupp

added theorem HahnSeries.SummableFamily.one_sub_self_mul_hsum_powers

added def HahnSeries.SummableFamily.powers

added theorem HahnSeries.SummableFamily.smul_apply

added theorem HahnSeries.SummableFamily.sub_apply

added theorem HahnSeries.SummableFamily.support_hsum_subset

added theorem HahnSeries.SummableFamily.zero_apply

added structure HahnSeries.SummableFamily

added def HahnSeries.addVal

added theorem HahnSeries.addVal_apply

added theorem HahnSeries.addVal_apply_of_ne

added theorem HahnSeries.addVal_le_of_coeff_ne_zero

added theorem HahnSeries.add_coeff'

added theorem HahnSeries.add_coeff

added theorem HahnSeries.algebraMap_apply'

added theorem HahnSeries.algebraMap_apply

added def HahnSeries.coeff.addMonoidHom

added def HahnSeries.coeff.linearMap

added theorem HahnSeries.coeff_eq_zero_of_lt_order

added theorem HahnSeries.coeff_fun_eq_zero_iff

added theorem HahnSeries.coeff_inj

added theorem HahnSeries.coeff_injective

added theorem HahnSeries.coeff_order_ne_zero

added theorem HahnSeries.coeff_toMvPowerSeries

added theorem HahnSeries.coeff_toMvPowerSeries_symm

added theorem HahnSeries.coeff_toPowerSeries

added theorem HahnSeries.coeff_toPowerSeries_symm

added def HahnSeries.embDomain

added def HahnSeries.embDomainAlgHom

added def HahnSeries.embDomainLinearMap

added def HahnSeries.embDomainRingHom

added theorem HahnSeries.embDomainRingHom_C

added theorem HahnSeries.embDomain_add

added theorem HahnSeries.embDomain_coeff

added theorem HahnSeries.embDomain_injective

added theorem HahnSeries.embDomain_mk_coeff

added theorem HahnSeries.embDomain_mul

added theorem HahnSeries.embDomain_notin_image_support

added theorem HahnSeries.embDomain_notin_range

added theorem HahnSeries.embDomain_one

added theorem HahnSeries.embDomain_single

added theorem HahnSeries.embDomain_smul

added theorem HahnSeries.embDomain_zero

added theorem HahnSeries.eq_of_mem_support_single

added theorem HahnSeries.isPwo_iUnion_support_powers

added theorem HahnSeries.isPwo_support

added theorem HahnSeries.isUnit_iff

added theorem HahnSeries.isWf_support

added theorem HahnSeries.mem_support

added theorem HahnSeries.min_order_le_order_add

added theorem HahnSeries.mul_coeff

added theorem HahnSeries.mul_coeff_left'

added theorem HahnSeries.mul_coeff_order_add_order

added theorem HahnSeries.mul_coeff_right'

added theorem HahnSeries.mul_single_coeff_add

added theorem HahnSeries.mul_single_zero_coeff

added theorem HahnSeries.ne_zero_of_coeff_ne_zero

added theorem HahnSeries.neg_coeff'

added theorem HahnSeries.neg_coeff

added def HahnSeries.ofPowerSeries

added def HahnSeries.ofPowerSeriesAlg

added theorem HahnSeries.ofPowerSeries_C

added theorem HahnSeries.ofPowerSeries_X

added theorem HahnSeries.ofPowerSeries_apply

added theorem HahnSeries.ofPowerSeries_apply_coeff

added theorem HahnSeries.ofPowerSeries_injective

added theorem HahnSeries.ofPowerSeries_x_pow

added theorem HahnSeries.one_coeff

added def HahnSeries.order

added theorem HahnSeries.order_C

added theorem HahnSeries.order_le_of_coeff_ne_zero

added theorem HahnSeries.order_mul

added theorem HahnSeries.order_neg

added theorem HahnSeries.order_of_ne

added theorem HahnSeries.order_one

added theorem HahnSeries.order_pow

added theorem HahnSeries.order_single

added theorem HahnSeries.order_zero

added def HahnSeries.single.addMonoidHom

added def HahnSeries.single.linearMap

added def HahnSeries.single

added theorem HahnSeries.single_coeff

added theorem HahnSeries.single_coeff_of_ne

added theorem HahnSeries.single_coeff_same

added theorem HahnSeries.single_eq_zero

added theorem HahnSeries.single_eq_zero_iff

added theorem HahnSeries.single_injective

added theorem HahnSeries.single_mul_coeff_add

added theorem HahnSeries.single_mul_single

added theorem HahnSeries.single_ne_zero

added theorem HahnSeries.single_zero_mul_coeff

added theorem HahnSeries.single_zero_mul_eq_smul

added theorem HahnSeries.single_zero_one

added theorem HahnSeries.smul_coeff

added theorem HahnSeries.sub_coeff'

added theorem HahnSeries.sub_coeff

added theorem HahnSeries.support_add_subset

added theorem HahnSeries.support_embDomain_subset

added theorem HahnSeries.support_eq_empty_iff

added theorem HahnSeries.support_mul_subset_add_support

added theorem HahnSeries.support_neg

added theorem HahnSeries.support_one

added theorem HahnSeries.support_single_of_ne

added theorem HahnSeries.support_single_subset

added theorem HahnSeries.support_zero

added def HahnSeries.toMvPowerSeries

added def HahnSeries.toPowerSeries

added def HahnSeries.toPowerSeriesAlg

added theorem HahnSeries.unit_aux

added theorem HahnSeries.zero_coeff

added structure HahnSeries

added theorem Polynomial.algebraMap_hahnSeries_apply

added theorem Polynomial.algebraMap_hahnSeries_injective

Modified Mathlib/RingTheory/Valuation/Basic.lean

modified theorem AddValuation.map_add'

modified theorem AddValuation.map_add

modified theorem AddValuation.map_eq_of_lt_sub

modified theorem AddValuation.map_inv

modified theorem AddValuation.map_mul

modified theorem AddValuation.map_pow

modified theorem AddValuation.map_sub

modified theorem AddValuation.top_iff