Commit 2025-05-09 18:56 d62eab0c

View on Github →

chore (RingTheory/HahnSeries/SummableFamily): refactor HahnSeries.SummableFamily.powers to take junk values (#22959) This PR removes the positive order condition on the function HahnSeries.SummableFamily.powers, and instead replaces the input with zero when the input has non-positive order. This follows a reviewer suggestion from #20205.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/HEval.lean

modified theorem HahnSeries.SummableFamily.hsum_powerSeriesFamily_mul

modified theorem HahnSeries.SummableFamily.powerSeriesFamily_add

deleted theorem HahnSeries.SummableFamily.powerSeriesFamily_apply

added theorem HahnSeries.SummableFamily.powerSeriesFamily_hsum_zero

added theorem HahnSeries.SummableFamily.powerSeriesFamily_of_not_orderTop_pos

added theorem HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos

modified theorem HahnSeries.SummableFamily.powerSeriesFamily_smul

modified theorem HahnSeries.SummableFamily.support_powerSeriesFamily_subset

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

modified theorem HahnSeries.SummableFamily.coe_powers

modified theorem HahnSeries.SummableFamily.coeff_hsum_mul

modified theorem HahnSeries.SummableFamily.hsum_mul

added theorem HahnSeries.SummableFamily.hsum_zero

modified theorem HahnSeries.SummableFamily.mul_eq_smul

modified theorem HahnSeries.SummableFamily.one_sub_self_mul_hsum_powers

modified def HahnSeries.SummableFamily.powers

added theorem HahnSeries.SummableFamily.powers_of_not_orderTop_pos

added theorem HahnSeries.SummableFamily.powers_of_orderTop_pos