English
For matrices a ∈ Matrix l m A and b ∈ Matrix m n A, the identity mulLeftLinearMap o R (a * b) = (mulLeftLinearMap o R a) .X (mulLeftLinearMap o R b) holds, i.e., left-linear map distributes over matrix multiplication via composition.
Русский
Для матриц a ∈ Matrix(l,m,A) и b ∈ Matrix(m,n,A) выполняется тождество mulLeftLinearMap o R (a · b) = (mulLeftLinearMap o R a) ∘ (mulLeftLinearMap o R b), т.е. левая линейная карта распределяется по умножению матриц через композицию.
LaTeX
$$$$mulLeftLinearMap o R (a * b) = (mulLeftLinearMap o R a).comp (mulLeftLinearMap o R b).$$$$
Lean4
/-- A version of `LinearMap.mulLeft_mul` for matrix multiplication. -/
@[simp]
theorem mulLeftLinearMap_mul [SMulCommClass R A A] (a : Matrix l m A) (b : Matrix m n A) :
mulLeftLinearMap o R (a * b) = (mulLeftLinearMap o R a).comp (mulLeftLinearMap o R b) :=
by
ext
simp only [mulLeftLinearMap_apply, LinearMap.comp_apply, Matrix.mul_assoc]
