# mathlib3documentation

linear_algebra.multilinear.basis

# Multilinear maps in relation to bases. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves lemmas about the action of multilinear maps on basis vectors.

## TODO #

• Refactor the proofs in terms of bases of tensor products, once there is an equivalent of basis.tensor_product for pi_tensor_product.
theorem basis.ext_multilinear_fin {R : Type u_1} {n : } {M : fin n Type u_3} {M₂ : Type u_4} [add_comm_monoid M₂] [Π (i : fin n), add_comm_monoid (M i)] [Π (i : fin n), (M i)] [ M₂] {f g : M₂} {ι₁ : fin n Type u_2} (e : Π (i : fin n), basis (ι₁ i) R (M i)) (h : (v : Π (i : fin n), ι₁ i), f (λ (i : fin n), (e i) (v i)) = g (λ (i : fin n), (e i) (v i))) :
f = g

Two multilinear maps indexed by fin n are equal if they are equal when all arguments are basis vectors.

theorem basis.ext_multilinear {R : Type u_1} {ι : Type u_2} {M₂ : Type u_4} {M₃ : Type u_5} [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₂] [ M₃] [finite ι] {f g : (λ (i : ι), M₂) M₃} {ι₁ : Type u_3} (e : basis ι₁ R M₂) (h : (v : ι ι₁), f (λ (i : ι), e (v i)) = g (λ (i : ι), e (v i))) :
f = g

Two multilinear maps indexed by a fintype are equal if they are equal when all arguments are basis vectors. Unlike basis.ext_multilinear_fin, this only uses a single basis; a dependently-typed version would still be true, but the proof would need a dependently-typed version of dom_dom_congr.