Theorems · Definition · linear algebra

LinearMap.linearEquivOfInjective

{K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {V₂ : Type v'} →
            [inst_3 : AddCommGroup V₂] →
              [inst_4 : Module K V₂] →
                [FiniteDimensional K V] →
                  [FiniteDimensional K V₂] →
                    (f : V →ₗ[K] V₂) → Function.Injective ⇑f → Module.finrank K V = Module.finrank K V₂ → V ≃ₗ[K] V₂

Given a linear map f between two vector spaces with the same dimension, if ker f = ⊥ then linearEquivOfInjective is the induced isomorphism between the two vector spaces.

Defined in

Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Cited by

3 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupModuleAddCommGroupModuleFiniteDimensionalFiniteDimensional