toLinAlgEquiv' — Mathlib

English

There is an algebra equivalence between n-by-n matrices and endomorphisms of R^n, realized by associating to a matrix its corresponding linear map and vice versa.

Русский

Существует алгебраическое эквивалентство между матрицами размера n×n над R и эндоморфизмами R^n, реализованное соответствием матрицы линейному отображению и наоборот.

LaTeX

$$$ toLinAlgEquiv' : \\mathrm{Mat}_{n\\times n}(R) \\simeq_{alg} \\mathrm{End}_R(R^n) $$$

Lean4

/-- A `Matrix n n R` is algebra equivalent to a linear map `(n → R) →ₗ[R] (n → R)`. -/
def toLinAlgEquiv' : Matrix n n R ≃ₐ[R] (n → R) →ₗ[R] n → R :=
  LinearMap.toMatrixAlgEquiv'.symm

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