English
For B a bilinear form on M and M,N suitable matrices, the product M · BilinForm.toMatrix b B · N equals the matrix of the bilinear form B composed with the corresponding linear maps induced by M^T and N in the target basis c.
Русский
Для билинейной формы B на M и подходящих матриц M,N выполняется равенство M · BilinForm.toMatrix b B · N = BilinForm.toMatrix c (B ∘ (Matrix.toLin c b M^T) ∘ (Matrix.toLin c b N)).
LaTeX
$$$$M \cdot \mathrm{BilinForm.toMatrix}_{b}(B) \cdot N = \mathrm{BilinForm.toMatrix}_{c}\bigl(B \circ (\mathrm{Matrix.toLin}_{c b} (M^{\top})) \circ (\mathrm{Matrix.toLin}_{c b} N)\bigr).$$$$
Lean4
theorem mul_toMatrix_mul (B : BilinForm R₁ M₁) (M : Matrix o n R₁) (N : Matrix n o R₁) :
M * BilinForm.toMatrix b B * N = BilinForm.toMatrix c (B.comp (Matrix.toLin c b Mᵀ) (Matrix.toLin c b N)) :=
LinearMap.mul_toMatrix₂_mul _ _ _ _ B _ _
