English
For a bilinear form B and matrices M,N, the bilinear form composed with the corresponding linear maps has matrix BilinForm.toMatrix c (P^T M^T N).
Русский
Для билинейной формы B и матриц M,N матрица композиции билинейной формы в базе c равна BilinForm.toMatrix c (P^T M^T N).
LaTeX
$$$$M \cdot \mathrm{toMatrix}_{b}(B) \cdot N = \mathrm{toMatrix}_{c}\bigl(B \circ (\mathrm{toLin}_{c b} (M^{T})) \circ (\mathrm{toLin}_{c b} N)\bigr).$$$$
Lean4
theorem toBilin_comp (M : Matrix n n R₁) (P Q : Matrix n o R₁) :
(Matrix.toBilin b M).comp (toLin c b P) (toLin c b Q) = Matrix.toBilin c (Pᵀ * M * Q) :=
by
ext x y
rw [Matrix.toBilin, BilinForm.toMatrix, Matrix.toBilin, BilinForm.toMatrix, toMatrix₂_symm, toMatrix₂_symm, ←
Matrix.toLinearMap₂_compl₁₂ b b c c]
simp
