Commit 2025-06-07 08:13 bd7f0d62

View on Github →

feat(HahnSeries): single_inv and single_div_single (#25414) This also renames SummableFamily.single to SummableFamily.const (matching Function.const) to make room for SummableFamily.single (matching Pi.single). Moves:

SummableFamily.single -> SummableFamily.const

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/HEval.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

added theorem HahnSeries.SummableFamily.coe_mk

added def HahnSeries.SummableFamily.const

modified theorem HahnSeries.SummableFamily.hsum_single

added theorem HahnSeries.SummableFamily.hsum_unique

modified theorem HahnSeries.SummableFamily.powers_of_not_orderTop_pos

added theorem HahnSeries.SummableFamily.powers_zero

modified def HahnSeries.SummableFamily.single

added theorem HahnSeries.inv_single

added theorem HahnSeries.single_div_single