Iterated product is multilinear

Stream: Is there code for X?

[Adam Topaz]

Does mathlib have a statement of the following form? Suppose that $R$ is a commutative semiring and $A$ is an $R$-algebra. Given function $\nu : \operatorname{fin} n \to A$, we may consider the iterated product $\prod_{i \in \operatorname{fin} n} \nu i$. This defines a multilinear map from $\operatorname{fin} n \to A$ to $A$.

In lean code, I'm looking for a term of type multilinear_map R (λ i : fin q, A) A.

(Ping: @Zhangir Azerbayev)

[Adam Topaz]

I found docs#multilinear_map.mk_pi_ring but this is for the semiring R itself.