Theorems · Definition · linear algebra

LinearMap.index

{M : Type u_1} →
  {N : Type u_2} →
    [inst : AddCommGroup M] →
      [inst_1 : AddCommGroup N] →
        {R : Type u_3} → [inst_2 : Ring R] → [inst_3 : Module R M] → [inst_4 : Module R N] → (M →ₗ[R] N) → ℤ

The index of a linear map with sign convention index = dim ker - dim coker. In the case that either the kernel or cokernel has infinite rank, the value is junk.

Defined in

Mathlib.Algebra.Module.LinearMap.Index

Cited by

11 results in Mathlib

Foundations

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

Assumes

AddCommGroupAddCommGroupRingModuleModule