toBilin'Aux_toMatrixAux — Mathlib

English

The map from BilinForm to Matrix and back again recovers the original BilinForm.

Русский

Из билинейной формы обратно в матрицу и снова в билинейную форму возвращает исходную билинейную форму.

LaTeX

$$$\text{toBilin'Aux_toMatrixAux}$$$

Lean4

theorem toBilin'Aux_toMatrixAux [DecidableEq n] (B₂ : BilinForm R₁ (n → R₁)) :
    Matrix.toBilin'Aux (BilinForm.toMatrixAux (fun j => Pi.single j 1) B₂) = B₂ := by
  rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux, toLinearMap₂'Aux_toMatrix₂Aux]

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