Theorems · Definition · linear algebra

Matrix.toLinearEquiv

{n : Type u_1} →
  [inst : Fintype n] →
    {R : Type u_2} →
      {M : Type u_3} →
        [inst_1 : CommRing R] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              Module.Basis n R M → [inst_4 : DecidableEq n] → (A : Matrix n n R) → IsUnit A.det → M ≃ₗ[R] M

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.

Defined in

Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Cited by

3 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeCommRingAddCommGroupModuleDecidableEq