Stream: Is there code for X?
Adam Topaz (Aug 12 2020 at 15:26):
Does mathlib have a statement of the following form? Suppose that is a commutative semiring and is an -algebra. Given function , we may consider the iterated product . This defines a multilinear map from to .
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
Last updated: May 07 2021 at 22:14 UTC