English
Let B be a bilinear form on M, and M denote a matrix acting on the left; then BilinForm.toMatrix b B times M yields the matrix of the bilinear form B after left-multiplying the first argument by the corresponding linear map.
Русский
Пусть B — билинейная форма на M, и M — соответствующая матрица, действующая слева; тогда BilinForm.toMatrix b B · M — это матрица билинейной формы после последовательного применения линейного отображения к первому аргументу.
LaTeX
$$$$\mathrm{BilinForm.toMatrix}_{b}(B) \cdot M = \mathrm{BilinForm.toMatrix}_{b}\bigl(B \circ (\mathrm{Matrix.toLin}_{b b} M^{\top})\bigr).$$$$
Lean4
theorem mul_toMatrix (B : BilinForm R₁ M₁) (M : Matrix n n R₁) :
M * BilinForm.toMatrix b B = BilinForm.toMatrix b (B.compLeft (Matrix.toLin b b Mᵀ)) :=
LinearMap.mul_toMatrix₂ _ _ _ B _
