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

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₂] [] [] [] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : Basis ι₁ R M) (b₂ : Basis ι₂ S N) {B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} {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.

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₂] [] [] [] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : Basis ι₁ R M) (b₂ : 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.

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} [] [] [] [] [Module Rₗ Mₗ] [Module Rₗ Nₗ] [Module Rₗ Pₗ] (b₁' : Basis ι₁ Rₗ Mₗ) (b₂' : 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.