Theorem HahnSeries.SummableFamily.powerSeriesFamily_add

Modification history

2025-05-09 18:56

Mathlib/RingTheory/HahnSeries/HEval.lean

chore (RingTheory/HahnSeries/SummableFamily): refactor HahnSeries.SummableFamily.powers to take junk values (#22959) …

Modified HahnSeries.SummableFamily.powerSeriesFamily_add View on Github →

2025-01-30 06:00

Mathlib/RingTheory/HahnSeries/HEval.lean

feat(RingTheory/HahnSeries): define powerSeriesFamily (#20205) …

Added HahnSeries.SummableFamily.powerSeriesFamily_add View on Github →