Theorems · Inductive type · functional analysis

NonnegSpectrumClass

(𝕜 : Type u_3) →
  (A : Type u_4) →
    [inst : CommSemiring 𝕜] → [PartialOrder 𝕜] → [inst_2 : NonUnitalRing A] → [PartialOrder A] → [Module 𝕜 A] → Prop

A class for 𝕜-algebras with a partial order where the ordering is compatible with the (quasi)spectrum.

Defined in

Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Cited by

292 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 45 definitions · uses no axioms

Assumes

CommSemiringPartialOrderNonUnitalRingPartialOrderModule