Commit 2024-10-22 21:35 9b02679b

View on Github →

feat (RingTheory/HahnSeries/Summable) : coeff function for a summable family (#16649) This PR introduces a coefficient function for summable families, and adds some basic formal sum results.

  • depends on: #16871 [single summable family]
  • depends on: #16872 [Equiv of families]

Estimated changes