English
The bilinear map represented by B, when multiplied on the left by M and on the right by N, corresponds to the bilinear map obtained by composing with the linear maps toLin' M^T and toLin' N.
Русский
Билинейное отображение, заданное B, при умножении слева на M и справа на N соответствует билинейному отображению, полученному через композицию с линейными отображениями toLin' M^T и toLin' N.
LaTeX
$$$M * B * N = B^{\mathrm{compl}_{1 2}}(toLin'(M^T), toLin'(N)).$$$
Lean4
/-- `LinearMap.toMatrix₂ b₁ b₂` is the equivalence between `R`-bilinear maps on `M` and
`n`-by-`m` matrices with entries in `R`, if `b₁` and `b₂` are `R`-bases for `M₁` and `M₂`,
respectively. -/
noncomputable def toMatrix₂ : (M₁ →ₗ[R] M₂ →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂ :=
(b₁.equivFun.arrowCongr (b₂.equivFun.arrowCongr (LinearEquiv.refl R N₂))).trans (LinearMap.toMatrix₂' R)
