Theorems · Theorem · commutative algebra
spectralValueTerms_bddAbove
∀ {R : Type u_1} [inst : SeminormedRing R] (p : Polynomial R), BddAbove (Set.range (spectralValueTerms p))The sequence spectralValue_terms p is bounded above.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Polynomialstatement and proof · cited by 5,681
- Set.rangestatement · cited by 4,705
- BddAbovestatement · cited by 620
- SeminormedRingstatement and proof · cited by 446
- Set.Finite.bddAboveproof · cited by 19
- spectralValueTermsstatement · cited by 8
- spectralValueTerms_finite_rangeproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- spectralNorm_nonnegproof · cited by 2
- spectralValue_eq_zero_iffproof · cited by 1
- spectralValue_le_one_iffproof · cited by 0