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.

Estimated changes