English
If A is invertible with respect to a basis b, then the associated linear equivalence on M given by toLin b b A is a bijection with inverse toLin b b A^{-1}.
Русский
Если A обратима по базису b, то соответствующее линейное эквивалентное отображение на M, заданное toLin b b A, является биекцией с обратным отображением toLin b b A^{-1}.
LaTeX
$$$A \\text{ invertible with } \\det A \\in R^\\times \\Rightarrow x \\mapsto (toLin(b,b,A)) x \\text{ is a linear equivalence with inverse } x \\mapsto (toLin(b,b,A^{-1})) x$$$
Lean4
/-- Given `hA : IsUnit A.det` and `b : Basis R b`, `A.toLinearEquiv b hA` is
the `LinearEquiv` arising from `toLin b b A`.
See `Matrix.toLinearEquiv'` for this result on `n → R`.
-/
@[simps apply]
noncomputable def toLinearEquiv [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) : M ≃ₗ[R] M
where
__ := toLin b b A
toFun := toLin b b A
invFun := toLin b b A⁻¹
left_inv
x := by
simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.nonsing_inv_mul _ hA, toLin_one,
LinearMap.id_apply]
right_inv
x := by
simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.mul_nonsing_inv _ hA, toLin_one,
LinearMap.id_apply]
