Commit 2025-02-19 11:45 16a1c5ce
View on Github →refactor(Analysis/Calculus/FormalMultilinearSeries): generalize to additive monoids (#9467) While many of the lemmas cease to apply, the definitions of sequences and their sums are still perfectly well-behaved in additive monoids; no negation is needed.