Commit 2024-10-18 14:51 2a3ae36b
View on Github →feat (RingTheory/HahnSeries/Summable) : transport summable families along Equiv (#16872) This PR defines a new summable family given a summable family of Hahn series and an equivalence of parametrizing types. We show that the new family has the same formal sum as the old one.