Multilinear maps in relation to bases. #
This file proves lemmas about the action of multilinear maps on basis vectors.
theorem
Basis.ext_multilinear
{ι : Type u_1}
{R : Type u_2}
[CommSemiring R]
{M : ι → Type u_3}
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
[Finite ι]
{f g : MultilinearMap R M N}
{ιM : ι → Type u_5}
(e : (i : ι) → Basis (ιM i) R (M i))
(h : ∀ (v : (i : ι) → ιM i), (f fun (i : ι) => (e i) (v i)) = g fun (i : ι) => (e i) (v i))
:
Two multilinear maps indexed by a Fintype are equal if they are equal when all arguments
are basis vectors.
@[deprecated Basis.ext_multilinear (since := "2025-05-12")]
theorem
Basis.ext_multilinear_fin
{ι : Type u_1}
{R : Type u_2}
[CommSemiring R]
{M : ι → Type u_3}
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
[Finite ι]
{f g : MultilinearMap R M N}
{ιM : ι → Type u_5}
(e : (i : ι) → Basis (ιM i) R (M i))
(h : ∀ (v : (i : ι) → ιM i), (f fun (i : ι) => (e i) (v i)) = g fun (i : ι) => (e i) (v i))
:
Alias of Basis.ext_multilinear.
Two multilinear maps indexed by a Fintype are equal if they are equal when all arguments
are basis vectors.