English
A bilinear construction with left and right linear maps yields a matrix equal to the matrix of the composed linear map with the corresponding P and Q inserted.
Русский
Построение через билинейность с левой и правой линейной вставкой даёт матрицу, равную матрице композиции с соответствующими P и Q.
LaTeX
$$$$ (\mathrm{Matrix.toLinearMap_2}\ b_1 b_2 M).\mathrm{compl}_{12} (toLin b_1' b_1 P) (toLin b_2' b_2 Q) = \mathrm{Matrix.toLinearMap_2' } b_1' b_2' (P^T \cdot M \cdot Q). $$$$
Lean4
theorem toLinearMap₂_compl₁₂ (M : Matrix n m R) (P : Matrix n n' R) (Q : Matrix m m' R) :
(Matrix.toLinearMap₂ b₁ b₂ M).compl₁₂ (toLin b₁' b₁ P) (toLin b₂' b₂ Q) =
Matrix.toLinearMap₂ b₁' b₂' (Pᵀ * M * Q) :=
(LinearMap.toMatrix₂ b₁' b₂').injective
(by simp only [LinearMap.toMatrix₂_compl₁₂ b₁ b₂, LinearMap.toMatrix₂_toLinearMap₂, toMatrix_toLin])
