Commit 2025-12-11 08:08 77a19484

View on Github →

chore: notation R⟦Γ⟧ = HahnSeries Γ R (#32670) As proposed on Zulip. This technically clashes with R⟦X⟧ for power series, but a similar clash already exists between R[G] for MonoidAlgebra and R[X] for Polynomial, so it should be fine.

Estimated changes

modified structure HahnEmbedding.IsPartial
modified theorem HahnSeries.coeff_add'
modified theorem HahnSeries.coeff_add
modified theorem HahnSeries.coeff_neg'
modified theorem HahnSeries.coeff_neg
modified theorem HahnSeries.coeff_nsmul
modified theorem HahnSeries.coeff_smul'
modified theorem HahnSeries.coeff_smul
modified theorem HahnSeries.coeff_sub'
modified theorem HahnSeries.coeff_sub
modified theorem HahnSeries.coeff_sum
modified theorem HahnSeries.embDomain_add
modified theorem HahnSeries.embDomain_smul
modified theorem HahnSeries.le_order_smul
modified theorem HahnSeries.leadingCoeff_neg
modified theorem HahnSeries.leadingCoeff_sub
modified theorem HahnSeries.orderTop_neg
modified theorem HahnSeries.orderTop_sub
modified theorem HahnSeries.orderTop_sub_ne
modified theorem HahnSeries.order_neg
modified theorem HahnSeries.support_neg
modified theorem HahnSeries.truncLT_add
modified theorem HahnSeries.truncLT_smul
modified theorem HahnSeries.coeff_inj
modified theorem HahnSeries.coeff_injective
modified theorem HahnSeries.coeff_zero'
modified theorem HahnSeries.coeff_zero
modified def HahnSeries.embDomain
modified theorem HahnSeries.embDomain_coeff
modified theorem HahnSeries.embDomain_zero
modified theorem HahnSeries.isPWO_support
modified theorem HahnSeries.isWF_support
modified theorem HahnSeries.leadingCoeff_eq
modified def HahnSeries.map
modified theorem HahnSeries.mem_support
modified def HahnSeries.ofFinsupp
modified def HahnSeries.ofIterate
modified def HahnSeries.order
modified def HahnSeries.orderTop
modified theorem HahnSeries.orderTop_zero
modified theorem HahnSeries.order_of_ne
modified theorem HahnSeries.order_zero
modified def HahnSeries.single
modified theorem HahnSeries.single_injective
modified theorem HahnSeries.support_zero
modified def HahnSeries.toIterate
modified def HahnSeries.truncLT
modified def PowerSeries.heval
modified theorem PowerSeries.heval_mul
modified theorem HahnSeries.leadingCoeff_abs
modified theorem HahnSeries.lt_iff
modified theorem HahnSeries.orderTop_abs
modified theorem HahnSeries.order_abs
modified theorem HahnSeries.support_abs
modified theorem HahnModule.add_smul
modified theorem HahnModule.coeff_smul
modified theorem HahnModule.coeff_smul_left
modified theorem HahnModule.coeff_smul_right
modified def HahnModule.of
modified theorem HahnModule.of_add
modified theorem HahnModule.of_smul
modified theorem HahnModule.of_sub
modified theorem HahnModule.of_zero
modified def HahnModule.rec
modified theorem HahnModule.smul_add
modified theorem HahnModule.zero_smul'
modified def HahnSeries.C
modified theorem HahnSeries.C_eq_algebraMap
modified theorem HahnSeries.C_injective
modified theorem HahnSeries.C_mul_eq_smul
modified theorem HahnSeries.C_ne_zero
modified theorem HahnSeries.C_one
modified theorem HahnSeries.C_zero
modified theorem HahnSeries.algebraMap_apply
modified theorem HahnSeries.coeff_mul
modified theorem HahnSeries.coeff_mul_left'
modified theorem HahnSeries.coeff_mul_right'
modified theorem HahnSeries.coeff_one
modified theorem HahnSeries.leadingCoeff_one
modified theorem HahnSeries.orderTop_one
modified theorem HahnSeries.order_C
modified theorem HahnSeries.order_one
modified theorem HahnSeries.support_one
modified structure HahnSeries.SummableFamily
modified theorem HahnSeries.isUnit_iff
modified theorem HahnSeries.unit_aux
modified def HahnSeries.addVal
modified theorem HahnSeries.addVal_apply