# Lemmas about bilinear maps with a basis over each argument #

source
theorem LinearMap.ext_basis {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {R₂ : Type u_4} {S : Type u_5} {S₂ : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [Semiring R] [Semiring S] [Semiring R₂] [Semiring S₂] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : Module.Basis ι₁ R M) (b₂ : Module.Basis ι₂ S N) {B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : ∀ (i : ι₁) (j : ι₂), (B (b₁ i)) (b₂ j) = (B' (b₁ i)) (b₂ j)) :
B = B'

Two bilinear maps are equal when they are equal on all basis vectors.

source
theorem LinearMap.sum_repr_mul_repr_mulₛₗ {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {R₂ : Type u_4} {S : Type u_5} {S₂ : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [Semiring R] [Semiring S] [Semiring R₂] [Semiring S₂] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : Module.Basis ι₁ R M) (b₂ : Module.Basis ι₂ S N) {B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (x : M) (y : N) :
((b₁.repr x).sum fun (i : ι₁) (xi : R) => (b₂.repr y).sum fun (j : ι₂) (yj : S) => ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) = (B x) y

Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis.

Version for semi-bilinear maps, see `sum_repr_mul_repr_mul` for the bilinear version.

source
theorem LinearMap.sum_repr_mul_repr_mul {ι₁ : Type u_1} {ι₂ : Type u_2} {Rₗ : Type u_10} {Mₗ : Type u_11} {Nₗ : Type u_12} {Pₗ : Type u_13} [CommSemiring Rₗ] [AddCommMonoid Mₗ] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module Rₗ Mₗ] [Module Rₗ Nₗ] [Module Rₗ Pₗ] (b₁' : Module.Basis ι₁ Rₗ Mₗ) (b₂' : Module.Basis ι₂ Rₗ Nₗ) {B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ} (x : Mₗ) (y : Nₗ) :
((b₁'.repr x).sum fun (i : ι₁) (xi : Rₗ) => (b₂'.repr y).sum fun (j : ι₂) (yj : Rₗ) => xi • yj • (B (b₁' i)) (b₂' j)) = (B x) y

Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis.

Version for bilinear maps, see `sum_repr_mul_repr_mulₛₗ` for the semi-bilinear version.