toBilin — Mathlib

English

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

Русский

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

LaTeX

$$(B.compRight f).toMatrix' = B.toMatrix' \cdot f.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 toBilin : Matrix n n R₁ ≃ₗ[R₁] BilinForm R₁ M₁ :=
  (BilinForm.toMatrix b).symm

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