English
A similar product rule describes multiplying on the left by M and using a transformed B with a ll transpose, yielding a matrix with new bases.
Русский
Похожее правило умножения описывает левое умножение на M и использование преобразованного B с транспонированием, дающее матрицу с иными основаниями.
LaTeX
$$$$ M \cdot \mathrm{toMatrix}_2^{b_1,b_2} (B) = \mathrm{toMatrix}_2^{b_1',b_2} \Bigl( B \; \mathrm{comp} \; (\mathrm{toLin}_{b_1',b_1} M^{\top}) \Bigr). $$$$
Lean4
theorem mul_toMatrix₂_mul (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) (N : Matrix m m' R) :
M * LinearMap.toMatrix₂ b₁ b₂ B * N = LinearMap.toMatrix₂ b₁' b₂' (B.compl₁₂ (toLin b₁' b₁ Mᵀ) (toLin b₂' b₂ N)) :=
by simp_rw [LinearMap.toMatrix₂_compl₁₂ b₁ b₂, toMatrix_toLin, transpose_transpose]
