toBilin_symm — Mathlib

English

The matrix of B composed on the left with f equals the transpose of the matrix of f times the matrix of B.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toBilin_symm : (Matrix.toBilin b).symm = BilinForm.toMatrix b :=
  (BilinForm.toMatrix b).symm_symm

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