mathlib3

21a96ef0 - feat(ring_theory/hahn_series): summable families of Hahn series (#6997)

feat(ring_theory/hahn_series): summable families of Hahn series (#6997) Defines `hahn_series.summable_family` Defines the formal sum `hahn_series.summable_family.hsum` and its linear map version, `hahn_series.summable_family.lsum` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>