One lemma of the spectrum of a linear map

This file just proves that the spectrum of a linear map is commutative.

theorem isUnit_comm (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [FiniteDimensional K E] (x : E →ₗ[K] E) (y : E →ₗ[K] E) : IsUnit (x ∘ₗ y) ↔ IsUnit (y ∘ₗ x)

theorem isUnit_neg {α : Type u_1} [Monoid α] [HasDistribNeg α] (x : α) : IsUnit (-x) ↔ IsUnit x

theorem spectrum.comm {K : Type u_1} {E : Type u_2} [Field K] [AddCommGroup E] [Module K E] [FiniteDimensional K E] (x : E →ₗ[K] E) (y : E →ₗ[K] E) : spectrum K (x ∘ₗ y) = spectrum K (y ∘ₗ x)