## Stream: Is there code for X?

### Topic: Iterated product is multilinear

#### Adam Topaz (Aug 12 2020 at 15:26):

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 (Aug 12 2020 at 15:39):

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

Last updated: May 07 2021 at 22:14 UTC