Theorems · Theorem · functional analysis
StarOrderedRing.nonneg_iff_quasispectrum_nonneg
∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
[inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalSemiring R] [inst_6 : ContinuousStar R]
[ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
[inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
[inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R A p]
[NonnegSpectrumClass R A] (a : A),
autoParam (p a) StarOrderedRing.nonneg_iff_quasispectrum_nonneg._auto_1 → (0 ≤ a ↔ ∀ x ∈ quasispectrum R a, 0 ≤ x)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Modulestatement and proof · cited by 20,661
- CommSemiringstatement and proof · cited by 10,911
- PartialOrderstatement and proof · cited by 6,410
- IsScalarTowerstatement and proof · cited by 3,896
- Nontrivialstatement and proof · cited by 2,416
- SMulCommClassstatement and proof · cited by 1,927
- StarRingstatement and proof · cited by 1,686
- MetricSpacestatement and proof · cited by 1,684
- StarOrderedRingstatement and proof · cited by 587
- NoZeroDivisorsstatement and proof · cited by 545
Cited by1
Results whose statement or proof uses this declaration.
- Unitization.inr_le_iffproof · cited by 8