Commit 2025-02-13 16:03 be6eed0b

View on Github →

feat: HasProd on sum types (#21683)

Estimated changes

Modified Mathlib/Data/Finset/Sum.lean

added def Finset.sumEquiv

added theorem Finset.sumEquiv_symm_apply

Modified Mathlib/Data/Set/Image.lean

added def Set.sumEquiv

Modified Mathlib/NumberTheory/LSeries/Linearity.lean

Modified Mathlib/Order/Filter/AtTopBot/Finset.lean

added theorem Filter.tendsto_toLeft_atTop

added theorem Filter.tendsto_toRight_atTop

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

added theorem tprod_finsetProd

deleted theorem tprod_of_prod

Modified Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean

added theorem HasProd.sum

added theorem Multipliable.sum

added theorem tprod_sum