toMatrixAlgEquiv' — Mathlib

English

Given inverses M and M', one obtains a linear isomorphism whose action and inverse are given by the corresponding toLin' maps.

Русский

При наличии обратных M, M' образуется линейное изоморфизмное отображение, действием которого являются соответствующие toLin'–карты, а обратное задано второй картой.

LaTeX

$$$ \\text{If } M M' = I \\text{ and } M' M = I, \\quad \\mathrm{toLin'}(M') \\text{ is an isomorphism with inverse } \\mathrm{toLin'}(M).$$$

Lean4

/-- Linear maps `(n → R) →ₗ[R] (n → R)` are algebra equivalent to `Matrix n n R`. -/
def toMatrixAlgEquiv' : ((n → R) →ₗ[R] n → R) ≃ₐ[R] Matrix n n R :=
  AlgEquiv.ofLinearEquiv LinearMap.toMatrix' LinearMap.toMatrix'_one LinearMap.toMatrix'_mul

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