toLinearEquiv'_symm_apply — Mathlib

English

The symmetric counterpart of the matrix-to-linear-equivalence correspondence: the inverse of P’s linear equivalence corresponds to the linear map given by P^{-1}.

Русский

Симметрический аналог соответствия между линейным отображением и матрицей: обратная линейного эквививалентного отображения соответствует линейному отображению, заданному P^{-1}.

LaTeX

$$$(P^{\\text{toLinearEquiv}'})^{-1} = (P^{-1})^{\\text{toLinearEquiv}'}$$$

Lean4

@[simp]
theorem toLinearEquiv'_symm_apply (P : Matrix n n R) (h : Invertible P) :
    (↑(P.toLinearEquiv' h).symm : Module.End R (n → R)) = Matrix.toLin' (⅟P) :=
  rfl

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