# mathlib3documentation

linear_algebra.basis.bilinear

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem linear_map.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} [comm_semiring R₂] [comm_semiring S₂] [ M] [ N] [module R₂ P] [module S₂ P] [ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : basis ι₁ R M) (b₂ : 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.

theorem linear_map.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} [comm_semiring R₂] [comm_semiring S₂] [ M] [ N] [module R₂ P] [module S₂ P] [ 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 (λ (i : ι₁) (xi : R), ((b₂.repr) y).sum (λ (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 linear_map.sum_repr_mul_repr_mul {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {Mₗ : Type u_10} {Nₗ : Type u_11} {Pₗ : Type u_12} [add_comm_monoid Mₗ] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [ Mₗ] [ Nₗ] [ Pₗ] (b₁' : basis ι₁ R Mₗ) (b₂' : basis ι₂ R Nₗ) {B : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} (x : Mₗ) (y : Nₗ) :
((b₁'.repr) x).sum (λ (i : ι₁) (xi : R), ((b₂'.repr) y).sum (λ (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.