toMatrixAlgEquiv'_symm — Mathlib

English

There is a reindexing-compatible form of toLin' expressed via the funCongrLeft construction.

Русский

Существует форма toLin', совместимая с переиндексацией, выражаемая через конструктор funCongrLeft.

LaTeX

$$$ \\mathrm{toLin'}(\\mathrm{reindex}\\, e_1\\, e_2\\, M) = \\uparrow(\\mathrm{LinearEquiv}.funCongrLeft\\, R\\, R\\, e_1^{\\mathrm{symm}}) \\ ∘_\\ell (\\mathrm{toLin'}\\, M) ∘_\\ell \\uparrow(\\mathrm{LinearEquiv}.funCongrLeft\\, R\\, R\\, e_2) $$$

Lean4

@[simp]
theorem toMatrixAlgEquiv'_symm : (LinearMap.toMatrixAlgEquiv'.symm : Matrix n n R ≃ₐ[R] _) = Matrix.toLinAlgEquiv' :=
  rfl

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