toLinearEquiv'_apply — Mathlib

English

Given a basis b of a finite-rank module M, and an invertible matrix A with det A ≠ 0, there is a linear equivalence M ≃ M whose matrix in the basis b is A, with inverse given by A^{-1}.

Русский

Пусть базис b модуля M конечного ранга и детерминант A не равен нулю; тогда существует линейное эквивалентность M ≃ M, чьей матрицей в базисе b является A, обратная же задаётся A^{-1}.

LaTeX

$$$A \\text{ invertible with } \\det A \\neq 0 \\Rightarrow \\text{the map } x \\mapsto (toLin\\,b\\,b\\,A) x \\text{ is a linear equivalence with inverse } x \\mapsto (toLin\\,b\\,b\\,A^{-1}) x$$$

Lean4

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

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