English
The bilinear-to-matrix equivalence is compatible with basis changes, i.e., changing bases on the domain and codomain corresponds to conjugation of the matrix by the basis-change matrices.
Русский
Эквиваленция билинейного отображения через матрицу совместима с изменением баз; изменение баз на области/области кодирования соответствует конъюгации матрицы матрицами смены баз.
LaTeX
$$$\mathrm{toMatrix}_2 \text{ commutes with basis changes: } B \mapsto [B] \mapsto B.$$$
Lean4
/-- `Matrix.toLinearMap₂ 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; this is the reverse direction of `LinearMap.toMatrix₂ b₁ b₂`. -/
noncomputable def toLinearMap₂ : Matrix n m N₂ ≃ₗ[R] M₁ →ₗ[R] M₂ →ₗ[R] N₂ :=
(LinearMap.toMatrix₂ b₁ b₂).symm
