mathlib3 documentation

monlib / linear_algebra.my_spec

One lemma of the spectrum of a linear map #

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

theorem is_unit_comm (K : Type u_1) (E : Type u_2) [division_ring K] [add_comm_group E] [module K E] [finite_dimensional K E] (x y : E →ₗ[K] E) :

is_unit (x.comp y) ↔ is_unit (y.comp x)

theorem is_unit_neg {α : Type u_1} [monoid α] [has_distrib_neg α] (x : α) :

is_unit (-x) ↔ is_unit x

theorem spectrum.comm {K : Type u_1} {E : Type u_2} [field K] [add_comm_group E] [module K E] [finite_dimensional K E] (x y : E →ₗ[K] E) :

spectrum K (x.comp y) = spectrum K (y.comp x)