Commit 2024-10-18 17:35 1ef8dd30
View on Github →feat (RingTheory/HahnSeries/Summable) : singleton summable family (#16871) This PR defines a summable family made of a single Hahn series, and shows that the formal sum of the family is equal to the original Hahn series.