Theorems · Theorem · functional analysis

spectrum_nonneg_of_nonneg

∀ {𝕜 : Type u_3} {A : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Ring A]
  [inst_3 : PartialOrder A] [inst_4 : Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] ⦃a : A⦄,
  0 ≤ a → ∀ ⦃x : 𝕜⦄, x ∈ spectrum 𝕜 a → 0 ≤ x

Defined in

Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringPartialOrderRingPartialOrderAlgebraNonnegSpectrumClass