toMatrixAux_eq — Mathlib

English

The auxiliary matrix-to-bilin equivalence aligns with the standard one; their evaluations coincide.

Русский

Вспомогательное соответствие матриц билинейной формы согласуется с обычным соответствием; их значения совпадают.

LaTeX

$$BilinForm.toMatrixAux (R₁ := R₁) b B = BilinForm.toMatrix b B$$

Lean4

theorem toMatrixAux_eq (B : BilinForm R₁ M₁) : BilinForm.toMatrixAux (R₁ := R₁) b B = BilinForm.toMatrix b B :=
  LinearMap.toMatrix₂Aux_eq _ _ B

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