Multilinear maps over finite dimensional spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The main results are that multilinear maps over finitely-generated, free modules are finitely-generated and free.
We do not put this in linear_algebra/multilinear_map/basic to avoid making the imports too large
there.
@[protected, instance]
def
module.finite.multilinear_map
{ι : Type u_1}
{R : Type u_2}
{M₂ : Type u_3}
{M₁ : ι → Type u_4}
[finite ι]
[comm_ring R]
[add_comm_group M₂]
[module R M₂]
[Π (i : ι), add_comm_group (M₁ i)]
[Π (i : ι), module R (M₁ i)]
[module.finite R M₂]
[module.free R M₂]
[∀ (i : ι), module.finite R (M₁ i)]
[∀ (i : ι), module.free R (M₁ i)] :
module.finite R (multilinear_map R M₁ M₂)
@[protected, instance]
def
module.free.multilinear_map
{ι : Type u_1}
{R : Type u_2}
{M₂ : Type u_3}
{M₁ : ι → Type u_4}
[finite ι]
[comm_ring R]
[add_comm_group M₂]
[module R M₂]
[Π (i : ι), add_comm_group (M₁ i)]
[Π (i : ι), module R (M₁ i)]
[module.finite R M₂]
[module.free R M₂]
[∀ (i : ι), module.finite R (M₁ i)]
[∀ (i : ι), module.free R (M₁ i)] :
module.free R (multilinear_map R M₁ M₂)