Commit 2024-10-25 17:41 159c3b56

View on Github →

feat (RingTheory/HahnSeries/Summable) : Pointwise SMul for summable families (#16701) This PR adds a definition and some API for pointwise SMul between summable families. This generalizes the action of a single Hahn series on a summable family.

depends on: #16649 [sundry API]
depends on: #16871 [single summable family]
depends on: #16872 [Equiv of families]

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

added def HahnSeries.SummableFamily.FamilySMul

added theorem HahnSeries.SummableFamily.family_smul_coeff

added theorem HahnSeries.SummableFamily.finite_co_support_prod_smul

added theorem HahnSeries.SummableFamily.hsum_family_smul

modified theorem HahnSeries.SummableFamily.hsum_smul

added theorem HahnSeries.SummableFamily.hsum_smul_module

added theorem HahnSeries.SummableFamily.isPWO_iUnion_support_prod_smul

modified theorem HahnSeries.SummableFamily.smul_apply

added theorem HahnSeries.SummableFamily.smul_eq

added theorem HahnSeries.SummableFamily.smul_support_finite

added theorem HahnSeries.SummableFamily.smul_support_subset_prod

added theorem HahnSeries.SummableFamily.sum_vAddAntidiagonal_eq