English
If e_i : M_i ≃ₗ[R] M_i' are linear isomorphisms for each i, then there is a linear equivalence between the spaces of multilinear maps induced by these domain isomorphisms.
Русский
Если для каждого i имеются линейные изоморфизмы e_i : M_i ≃ M_i', то существует линейное эквивалентное отображение между пространствами мультиленейных отображений, индуцированное этими изоморфизмами доменов.
LaTeX
$$$$\bigl( \prod_{i} (M_i \simeq M_i') \bigr) \Rightarrow ( MultilinearMap(R, M_1', M_2) \simeq (MultilinearMap(R, M_1, M_2)) ).$$$$
Lean4
/-- Given an `R`-algebra `A`, `mkPiAlgebraFin` is the multilinear map on `A^n` associating
to `m` the product of all the `m i`.
See also `MultilinearMap.mkPiAlgebra` for a version that assumes `[CommSemiring A]` but works
for `A^ι` with any finite type `ι`. -/
protected def mkPiAlgebraFin : MultilinearMap R (fun _ : Fin n => A) A :=
MultilinearMap.mk' (fun m ↦ (List.ofFn m).prod)
(fun m i x y ↦ by
simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set, add_mul, mul_add, add_mul])
(fun m i c x ↦ by simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set])
