toMatrixAlgEquiv'_toLinAlgEquiv' — Mathlib

English

If M and M' are mutual inverses, then Matrix.toLin' M' is a linear equivalence with inverse Matrix.toLin' M.

Русский

Если M и M' взаимно обратны, то Matrix.toLin' M' является линейным эквивалентом с обратной связью Matrix.toLin' M.

LaTeX

$$$ \\text{If } M M' = 1 \\text{ and } M' M = 1, \\text{ then } \\mathrm{toLin'}(M') \\text{ is a linear equivalence with inverse } \\mathrm{toLin'}(M). $$$

Lean4

@[simp]
theorem toMatrixAlgEquiv'_toLinAlgEquiv' (M : Matrix n n R) :
    LinearMap.toMatrixAlgEquiv' (Matrix.toLinAlgEquiv' M) = M :=
  LinearMap.toMatrixAlgEquiv'.apply_symm_apply M

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