Values of a multilinear map on spans

A multilinear map is linear in each argument separately, so its value at a family of arguments drawn from the spans of sets s i is a linear combination of its values at families drawn from the sets s i themselves. This is the multilinear analogue of Submodule.map₂_span_span for bilinear maps. It reduces statements about all values of a determinant-like expression to its values on generators.

Main results

• MultilinearMap.map_mem_span_image_pi: if m i ∈ span R (s i) for every i, then f m lies in the span of the values of f on Set.univ.pi s.

theorem MultilinearMap.map_mem_span_image_pi {R : Type u_1} {ι : Type u_2} {N : Type u_3} {M : ι → Type u_4} [Semiring R] [Finite ι] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] (f : MultilinearMap R M N) (s : (i : ι) → Set (M i)) {m : (i : ι) → M i} (hm : ∀ (i : ι), m i ∈ Submodule.span R (s i)) : f m ∈ Submodule.span R (⇑f '' Set.univ.pi s)

The value of a multilinear map at arguments drawn from the spans of sets s i lies in the span of its values at arguments drawn from the sets s i.