English
The multilinermap mkPiAlgebra evaluated at a tuple m of elements of A equals the product of all coordinates: ∏ i m_i.
Русский
Мультиляневная карта mkPiAlgebra, примененная к кортежу m из элементов A, равна произведению всех координат: ∏ i m_i.
LaTeX
$$$\mathrm{mkPiAlgebra}_{R,\,\iota, A}(m) = \prod_i m_i$$$
Lean4
/-- Given an `R`-algebra `A`, `mkPiAlgebra` is the multilinear map on `A^ι` associating
to `m` the product of all the `m i`.
See also `MultilinearMap.mkPiAlgebraFin` for a version that works with a non-commutative
algebra `A` but requires `ι = Fin n`. -/
protected def mkPiAlgebra : MultilinearMap R (fun _ : ι => A) A
where
toFun m := ∏ i, m i
map_update_add' m i x y := by simp [Finset.prod_update_of_mem, add_mul]
map_update_smul' m i c x := by simp [Finset.prod_update_of_mem]
