Bilinear maps on finite linear combinations #
A bilinear map evaluated on two finite linear combinations ∑ k ∈ s, c k • φ k and
∑ l ∈ t, d l • ψ l expands as the double sum ∑ k ∈ s, ∑ l ∈ t, c k • d l • B (φ k) (ψ l).
This is the expansion along arbitrary families of vectors, rather than along a basis as in
Mathlib's LinearMap.sum_repr_mul_repr_mul.
theorem
LinearMap.apply_sum_smul_sum_smul
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{ι : Type u_5}
{κ : Type u_6}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(B : M →ₗ[R] N →ₗ[R] P)
(s : Finset ι)
(t : Finset κ)
(c : ι → R)
(φ : ι → M)
(d : κ → R)
(ψ : κ → N)
:
A bilinear map evaluated on two finite linear combinations is the double sum of its values on the summands.