Multilinear maps over finite dimensional spaces #
The main results are that multilinear maps over finitely-generated, free modules are finitely-generated and free.
We do not put this in LinearAlgebra.Multilinear.Basic to avoid making the imports too large
there.
instance
Module.Finite.multilinearMap
{ι : Type u_1}
{R : Type u_2}
{M₂ : Type u_3}
{M₁ : ι → Type u_4}
[Finite ι]
[CommRing R]
[AddCommGroup M₂]
[Module R M₂]
[Module.Finite R M₂]
[Module.Free R M₂]
[(i : ι) → AddCommGroup (M₁ i)]
[(i : ι) → Module R (M₁ i)]
[∀ (i : ι), Module.Finite R (M₁ i)]
[∀ (i : ι), Module.Free R (M₁ i)]
:
Module.Finite R (MultilinearMap R M₁ M₂)
instance
Module.Free.multilinearMap
{ι : Type u_1}
{R : Type u_2}
{M₂ : Type u_3}
{M₁ : ι → Type u_4}
[Finite ι]
[CommRing R]
[AddCommGroup M₂]
[Module R M₂]
[Module.Finite R M₂]
[Module.Free R M₂]
[(i : ι) → AddCommGroup (M₁ i)]
[(i : ι) → Module R (M₁ i)]
[∀ (i : ι), Module.Finite R (M₁ i)]
[∀ (i : ι), Module.Free R (M₁ i)]
:
Module.Free R (MultilinearMap R M₁ M₂)