mathlib documentation

linear_algebra.multilinear.basis

Multilinear maps in relation to bases. #

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

TODO #

theorem basis.ext_multilinear_fin {R : Type u_1} {n : } {M : fin nType u_3} {M₂ : Type u_4} [comm_semiring R] [add_comm_monoid M₂] [Π (i : fin n), add_comm_monoid (M i)] [Π (i : fin n), module R (M i)] [module R M₂] {f g : multilinear_map R M M₂} {ι₁ : fin nType 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} [comm_semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M₂] [module R M₃] [decidable_eq ι] [fintype ι] {f g : multilinear_map R (λ (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.