Theorem SummationFilter.HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc

Modification history

2025-11-04 09:42
Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean
feat: Ixx summation filters (#30380) …
Added SummationFilter.HasProd.hasProd_symmetricIco_of_hasProd_symmetricIccView on Github →