mathlib documentation

linear_algebra.multilinear.finite_dimensional

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 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} [decidable_eq ι] [fintype ι] [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)] :
@[protected, instance]
def module.free.multilinear_map {ι : Type u_1} {R : Type u_2} {M₂ : Type u_3} {M₁ : ι → Type u_4} [decidable_eq ι] [fintype ι] [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)] :