toContinuousLinearEquivOfDetNeZero

English

The linear map on the two-dimensional product space corresponding to the 2×2 matrix [[a,b],[c,d]] is the map (x,y) ↦ (a x + b y, c x + d y) relative to the standard two-coordinate basis.

Русский

Линейное отображение на пространстве двойной размерности, соответствующее матрице [[a,b],[c,d]], есть отображение (x,y) ↦ (a x + b y, c x + d y) по отношению к стандартному базису.

LaTeX

$$$\\forall a,b,c,d \\in 𝕜:\\; \\text{the linear map associated to }\\begin{pmatrix}a&b\\\\ c&d\\end{pmatrix} \\text{ is } (x,y) \\mapsto (a x + b y, c x + d y).$$$

Lean4

/-- Builds a continuous linear equivalence from a continuous linear map on a finite-dimensional
vector space whose determinant is nonzero. -/
def toContinuousLinearEquivOfDetNeZero (f : E →L[𝕜] E) (hf : f.det ≠ 0) : E ≃L[𝕜] E :=
  ((f : E →ₗ[𝕜] E).equivOfDetNeZero hf).toContinuousLinearEquiv

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