toBilin'Aux_single — Mathlib

English

The composite from BilinForm to Matrix and back yields the original BilinForm.

Русский

Композиция BilinForm → Matrix → BilinForm восстанавливает исходную билинейную форму.

LaTeX

$$$ Matrix.toBilin'Aux (BilinForm.toMatrixAux (fun j => \Pi.single j 1) B_2) = B_2 $$$

Lean4

theorem toBilin'Aux_single [Fintype n] [DecidableEq n] (M : Matrix n n R₁) (i j : n) :
    M.toBilin'Aux (Pi.single i 1) (Pi.single j 1) = M i j :=
  Matrix.toLinearMap₂'Aux_single _ _ _ _ _

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