toLinAlgEquiv'_toMatrixAlgEquiv' — Mathlib

English

The inverse equivalence matches the forward equivalence in both directions.

Русский

Обратное эквивалентство согласуется с прямым во всех направлениях.

LaTeX

$$$ \\mathrm{toLinAlgEquiv'}(\\mathrm{LinearMap.toMatrixAlgEquiv'}(f)) = f $$$

Lean4

@[simp]
theorem toLinAlgEquiv'_toMatrixAlgEquiv' (f : (n → R) →ₗ[R] n → R) :
    Matrix.toLinAlgEquiv' (LinearMap.toMatrixAlgEquiv' f) = f :=
  Matrix.toLinAlgEquiv'.apply_symm_apply f

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