Index of linear maps

This file extends Mathlib's algebraic LinearMap.index API with its invariance under composing with a linear equivalence.

These composition lemmas are absent from Mathlib.Algebra.Module.LinearMap.Index and support the continuous-linear-map results in TauCeti.Analysis.Fredholm.Index.

@[simp]

theorem LinearMap.index_equiv_comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (e : N ≃ₗ[R] P) : (↑e ∘ₗ f).index = f.index

Postcomposition with a linear equivalence leaves the index unchanged.

@[simp]

theorem LinearMap.index_comp_equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (e : P ≃ₗ[R] M) : (f ∘ₗ ↑e).index = f.index

Precomposition with a linear equivalence leaves the index unchanged.