toMatrix — Mathlib

English

The matrix of the left-composed bilinear form equals the transpose of the matrix of f times the matrix of B.

Русский

Матрица билинейной формы после левой композиции равна транспонированной матрице f, умноженной на матрицу B.

LaTeX

$$(B.compLeft f).toMatrix' = f.toMatrix'^{\top} \cdot B.toMatrix'$$

Lean4

/-- `BilinForm.toMatrix b` is the equivalence between `R`-bilinear forms on `M` and
`n`-by-`n` matrices with entries in `R`, if `b` is an `R`-basis for `M`. -/
noncomputable def toMatrix : BilinForm R₁ M₁ ≃ₗ[R₁] Matrix n n R₁ :=
  LinearMap.toMatrix₂ b b

Похожие утверждения