Theorems · Theorem · field theory

spectrum.nonempty_of_isAlgClosed_of_finiteDimensional

∀ (𝕜 : Type u) {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [IsAlgClosed 𝕜] [Nontrivial A]
  [I : FiniteDimensional 𝕜 A] (a : A), (spectrum 𝕜 a).Nonempty

Every element a in a nontrivial finite-dimensional algebra A over an algebraically closed field 𝕜 has non-empty spectrum.

Defined in

Mathlib.FieldTheory.IsAlgClosed.Spectrum

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldRingAlgebraIsAlgClosedNontrivialFiniteDimensional