Commit 2024-12-23 11:30 86975ccf

View on Github →

chore(RingTheory/HahnSeries/Summable): refactor powers (#20187) This PR removes the IsDomain hypothesis from the definition of the summable family powers.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

added theorem HahnSeries.SummableFamily.co_support_zero

added theorem HahnSeries.SummableFamily.isPWO_iUnion_support_powers

added theorem HahnSeries.SummableFamily.pow_finite_co_support

added theorem HahnSeries.SummableFamily.support_pow_subset_closure

deleted theorem HahnSeries.isPWO_iUnion_support_powers