Products of matrix units

Matrix.single_mul_single_eq_ite combines the matching-index and unequal-index product identities into one formula for rectangular matrix units with arbitrary coefficients. Only the shared index type needs to be finite. Matrix.smul_vecMulVec_single_single writes a scaled outer product of two coordinate vectors as a matrix unit, and Matrix.one_add_single_mul_one_add_single_of_ne multiplies two elementary matrices 1 + c Eᵢⱼ and 1 + d Eₖₗ with j ≠ k, whose cross term vanishes. LinearMap.apply_eq_sum_sum_smul_single expands a linear map on matrices along the matrix units.

theorem Matrix.single_mul_single_eq_ite {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_4} [NonUnitalNonAssocSemiring R] [DecidableEq l] [DecidableEq m] [DecidableEq n] [Fintype m] (i : l) (j k : m) (a : n) (c d : R) : single i j c * single k a d = if j = k then single i a (c * d) else 0

The product of two matrix units vanishes unless their inner indices agree.

theorem Matrix.smul_vecMulVec_single_single {m : Type u_1} {n : Type u_2} {R : Type u_3} [MulZeroOneClass R] [DecidableEq m] [DecidableEq n] (i : m) (j : n) (c : R) : c • vecMulVec (Pi.single i 1) (Pi.single j 1) = single i j c

A scaled outer product of two coordinate vectors is a matrix unit.

theorem Matrix.one_add_single_mul_one_add_single_of_ne {n : Type u_1} {R : Type u_2} [NonAssocSemiring R] [DecidableEq n] [Fintype n] {i j k l : n} (h : j ≠ k) (c d : R) : (1 + single i j c) * (1 + single k l d) = 1 + single i j c + single k l d

Two elementary matrices 1 + c Eᵢⱼ and 1 + d Eₖₗ multiply without a cross term when the column j of the first differs from the row k of the second.

theorem LinearMap.apply_eq_sum_sum_smul_single {ι : Type u_1} {κ : Type u_2} {R : Type u_3} {M : Type u_4} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] [Semiring R] [AddCommMonoid M] [Module R M] (f : Matrix ι κ R →ₗ[R] M) (A : Matrix ι κ R) : f A = ∑ i : ι, ∑ j : κ, A i j • f (Matrix.single i j 1)

A linear map on matrices is determined by its values on the matrix units: it sends A to the sum of A i j • f (single i j 1).