Zulip Chat Archive

Stream: Is there code for X?

Topic: Iterated product is multilinear


view this post on Zulip Adam Topaz (Aug 12 2020 at 15:26):

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

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

(Ping: @Zhangir Azerbayev)

view this post on Zulip 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