English
For matrices a and b of appropriate sizes, the linear map obtained by first left-multiplying by a and then right-multiplying by b equals the linear map obtained by first right-multiplying by b and then left-multiplying by a; i.e., L_a ∘ R_b = R_b ∘ L_a.
Русский
Для матриц A и B подходящих размеров линейное отображение, задаваемое сначала левым умножением на A, затем правым умножением на B, равно отображению, задаваемому сначала правым умножением на B, затем левым умножением на A; то есть L_A ∘ R_B = R_B ∘ L_A.
LaTeX
$$$\big(\operatorname{mulLeftLinearMap}\ o\ R\ a\big) \circ\big(\operatorname{mulRightLinearMap}\ m\ R\ b\big) = \big(\operatorname{mulRightLinearMap}\ l\ R\ b\big) \circ\big(\operatorname{mulLeftLinearMap}\ n\ R\ a\big)$$$
Lean4
/-- A version of `LinearMap.commute_mulLeft_right` for matrix multiplication. -/
theorem commute_mulLeftLinearMap_mulRightLinearMap (a : Matrix l m A) (b : Matrix n o A) :
mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b = mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a :=
by
ext c : 1
exact (Matrix.mul_assoc a c b).symm
