Commit 2025-02-03 16:47 89c8ee9c

View on Github →

chore(InfiniteSum/NatInt): put Multipliable.tendsto_prod_tprod_nat in the right namespace (#21337) Before, it was:

HasProd.Multipliable.tendsto_prod_tprod_nat

which made the additive version

HasSum.Multipliable.tendsto_sum_tsum_nat

By lifting into the root namespace, Multipliable properly additivizes

Estimated changes