invertibleToMatrix — Mathlib

English

The mapping sending b to b' defines an invertible matrix.

Русский

Определяемая матрица перехода между базисами является обратимой, её обратная — матрица перехода в противоположном направлении.

LaTeX

$$def invertibleToMatrix (b b' : Basis ι R₂ M₂) : Invertible (b.toMatrix b')$$

Lean4

/-- A matrix whose columns form a basis `b'`, expressed w.r.t. a basis `b`, is invertible. -/
def invertibleToMatrix [DecidableEq ι] [Fintype ι] (b b' : Basis ι R₂ M₂) : Invertible (b.toMatrix b') :=
  ⟨b'.toMatrix b, toMatrix_mul_toMatrix_flip _ _, toMatrix_mul_toMatrix_flip _ _⟩

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