Commit 2024-12-03 14:52 a8931809

View on Github →

feat (RingTheory/HahnSeries/Summable) add pointwise product operation (#18794) This PR defines a pointwise product operation on summable families of Hahn series, and shows that the formal sum of the pointwise product is equal to the product of formal sums. This is preparation for defining algebra homomorphisms from power series rings.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

deleted def HahnSeries.SummableFamily.FamilySMul

deleted theorem HahnSeries.SummableFamily.family_smul_coeff

added theorem HahnSeries.SummableFamily.finite_co_support_prod_mul

deleted theorem HahnSeries.SummableFamily.hsum_family_smul

added theorem HahnSeries.SummableFamily.hsum_mul

added theorem HahnSeries.SummableFamily.isPWO_iUnion_support_prod_mul

added def HahnSeries.SummableFamily.mul

added theorem HahnSeries.SummableFamily.mul_coeff

added theorem HahnSeries.SummableFamily.mul_eq_smul

added def HahnSeries.SummableFamily.smul

added theorem HahnSeries.SummableFamily.smul_coeff

added theorem HahnSeries.SummableFamily.smul_hsum