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