toBilin'_toMatrix' — Mathlib

English

The round-trip of BilinForm and Matrix toMatrix' is the identity; applying toBilin' to a BilinForm then toMatrix' brings you back to the original BilinForm.

Русский

Возврат между BilinForm и Matrix через toMatrix' даёт тождество; применение toBilin' к BilinForm затем toMatrix' возвращает исходную BilinForm.

LaTeX

$$$\text{toBilin'_toMatrix'} : B \mapsto B$$$

Lean4

@[simp]
theorem toBilin'_toMatrix' (B : BilinForm R₁ (n → R₁)) : Matrix.toBilin' (BilinForm.toMatrix' B) = B :=
  Matrix.toBilin'.apply_symm_apply B

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