Infinite product

Stream: Is there code for X?

[Ella Yu]

Hi, I am trying to define a Riemann zeta function as an infinite product. Is there a code for this just like tsum? Thank you!

[Eric Wieser]

You could take the docs#tsum of docs#additive (something like (∑' a, additive.of_mul (f a)).to_mul) , but that's unlikely to be very pleasant

[Ella Yu]

Thanks a lot! But my f a here is complex, is there a complex.to_mul or something equivalent?

[Eric Wieser]

The code above should work for complex

[Eric Wieser]

Note the parens; that's additive.to_mul that's being called (via dot notation)

[Kevin Buzzard]

Is the actual correct thing to do to make tprod and then define tsum via to_additive?

[Eric Wieser]

Probably yes

[Eric Wieser]

Although tprod already means "tensor product" so we have a naming problem conceptually (I think namespaces save us for now)