Commit 2024-02-16 04:51 e4037a3e

View on Github →

chore: Split HahnSeries file (#10595) The HahnSeries file is approaching 2000 lines, and I was hoping to add some more material on Hahn series in the near future. This PR splits the material roughly according to what structure we see in the coefficients: Basic assumes that the coefficient type R has zero, Addition assumes addition, Multiplication more or less assumes some multiplicative structure.

Estimated changes

deleted theorem HahnModule.ext
deleted def HahnModule.of
deleted theorem HahnModule.of_add
deleted theorem HahnModule.of_symm_add
deleted theorem HahnModule.of_symm_zero
deleted theorem HahnModule.of_zero
deleted def HahnModule.rec
deleted theorem HahnModule.smul_coeff
deleted def HahnModule
deleted def HahnSeries.C
deleted theorem HahnSeries.C_injective
deleted theorem HahnSeries.C_mul_eq_smul
deleted theorem HahnSeries.C_ne_zero
deleted theorem HahnSeries.C_one
deleted theorem HahnSeries.C_zero
deleted structure HahnSeries.SummableFamily
deleted def HahnSeries.addVal
deleted theorem HahnSeries.addVal_apply
deleted theorem HahnSeries.add_coeff'
deleted theorem HahnSeries.add_coeff
deleted theorem HahnSeries.coeff_inj
deleted theorem HahnSeries.embDomain_add
deleted theorem HahnSeries.embDomain_mul
deleted theorem HahnSeries.embDomain_one
deleted theorem HahnSeries.embDomain_smul
deleted theorem HahnSeries.embDomain_zero
deleted theorem HahnSeries.isPWO_support
deleted theorem HahnSeries.isUnit_iff
deleted theorem HahnSeries.isWF_support
deleted theorem HahnSeries.le_order_smul
deleted theorem HahnSeries.mem_support
deleted theorem HahnSeries.mul_coeff
deleted theorem HahnSeries.neg_coeff'
deleted theorem HahnSeries.neg_coeff
deleted theorem HahnSeries.one_coeff
deleted def HahnSeries.order
deleted theorem HahnSeries.order_C
deleted theorem HahnSeries.order_mul
deleted theorem HahnSeries.order_neg
deleted theorem HahnSeries.order_of_ne
deleted theorem HahnSeries.order_one
deleted theorem HahnSeries.order_pow
deleted theorem HahnSeries.order_single
deleted theorem HahnSeries.order_zero
deleted def HahnSeries.single
deleted theorem HahnSeries.single_coeff
deleted theorem HahnSeries.single_eq_zero
deleted theorem HahnSeries.single_ne_zero
deleted theorem HahnSeries.smul_coeff
deleted theorem HahnSeries.sub_coeff'
deleted theorem HahnSeries.sub_coeff
deleted theorem HahnSeries.support_neg
deleted theorem HahnSeries.support_one
deleted theorem HahnSeries.support_zero
deleted theorem HahnSeries.unit_aux
deleted theorem HahnSeries.zero_coeff
deleted structure HahnSeries
added theorem HahnSeries.add_coeff'
added theorem HahnSeries.add_coeff
added theorem HahnSeries.neg_coeff'
added theorem HahnSeries.neg_coeff
added theorem HahnSeries.order_neg
added theorem HahnSeries.smul_coeff
added theorem HahnSeries.sub_coeff'
added theorem HahnSeries.sub_coeff
added theorem HahnSeries.support_neg
added theorem HahnSeries.coeff_inj
added theorem HahnSeries.mem_support
added def HahnSeries.order
added theorem HahnSeries.order_of_ne
added theorem HahnSeries.order_zero
added theorem HahnSeries.zero_coeff
added structure HahnSeries
added theorem HahnModule.ext
added def HahnModule.of
added theorem HahnModule.of_add
added theorem HahnModule.of_symm_add
added theorem HahnModule.of_zero
added def HahnModule.rec
added theorem HahnModule.smul_coeff
added def HahnModule
added def HahnSeries.C
added theorem HahnSeries.C_injective
added theorem HahnSeries.C_ne_zero
added theorem HahnSeries.C_one
added theorem HahnSeries.C_zero
added theorem HahnSeries.mul_coeff
added theorem HahnSeries.one_coeff
added theorem HahnSeries.order_C
added theorem HahnSeries.order_mul
added theorem HahnSeries.order_one
added theorem HahnSeries.order_pow
added theorem HahnSeries.support_one
added structure HahnSeries.SummableFamily
added theorem HahnSeries.isUnit_iff
added theorem HahnSeries.unit_aux