Theorem LSeriesHasSum.sum

Modification history

2024-11-13 20:45
Mathlib/NumberTheory/LSeries/Linearity.lean
feat: LSeries commutes with finite sums (#18928) …
Added LSeriesHasSum.sumView on Github →