toLinearMapₛₗ₂'_aux_eq — Mathlib

English

The two-way constructions between bilinear maps and matrices form an equivalence; applying both directions returns the original bilinear map.

Русский

Две цепи преобразований между билинейными отображениями и матрицами образуют эквивалентность; применение обеих сторон возвращает исходное билинейное отображение.

LaTeX

$$$\text{toMatrix₂Aux} \circ \text{toLinearMap₂'Aux} = \text{id}$ and vice versa$$

Lean4

theorem toLinearMapₛₗ₂'_aux_eq (M : Matrix n m N₂) :
    Matrix.toLinearMap₂'Aux σ₁ σ₂ M = Matrix.toLinearMapₛₗ₂' R σ₁ σ₂ M :=
  rfl

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