Structures · Algebra
NonnegSpectrumClass
A class for 𝕜-algebras with a partial order where the ordering is compatible with the
(quasi)spectrum.
- Shape
- 2 explicit arguments · adds quasispectrum_nonneg_of_nonneg
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Real
- Complex
How is a type an instance?
Loading the hierarchy index…
Assumed by299
- CFC.sqrt
- CFC.abs
- CFC.conjSqrt
- CFC.sqrt_nonneg
- CFC.sqrt_mul_sqrt_self
- cfcₙ_nnreal_eq_real
- cfc_nnreal_eq_real
- NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg
- CFC.sqrt_eq_iff
- CFC.sqrt_eq_nnrpow
- CFC.sqrt.congr_simp
- CFC.rpow_zero
- CFC.sqrt_eq_rpow
- CFC.rpow_def
- CFC.rpow
- CStarAlgebra.isStrictlyPositive_TFAE
- cfc_le_iff
- CFC.nnrpow_one
- CStarAlgebra.nonneg_TFAE
- CFC.abs.congr_simp
- CFC.nnrpow
- CFC.abs_mul_abs
- CFC.rpow_rpow
- CFC.nnrpow_eq_rpow
- CFC.sqrt_eq_cfc
- IsGreatest.nnnorm_cfcₙ_nnreal
- SpectrumRestricts.nnreal_of_nonneg
- QuasispectrumRestricts.nnreal_of_nonneg
- spectrum_nonneg_of_nonneg
- CFC.nnrpow_nnrpow
- IsGreatest.nnnorm_cfc_nnreal
- nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
- CFC.sqrt_mul_self
- CFC.sqrt_one
- CFC.rpow_neg_one_eq_inv
- CFC.rpow_add
- CFC.inverse_eq_rpow_neg_one
- CFC.nnrpow_zero
- CFC.abs_eq_cfcₙ_coe_norm
- IsStrictlyPositive.spectrum_pos
- apply_le_nnnorm_cfcₙ_nnreal
- algebraMap_le_iff_le_spectrum
- cfcHom_nonneg_iff
- cfcₙ_nonneg_iff
- ContinuousOn.cfcₙ_nnreal
- CStarAlgebra.nonneg_iff_eq_star_mul_self
- CFC.nnrpow_two
- CFC.sqrt_of_not_nonneg
- apply_le_nnnorm_cfc_nnreal
- cfc_nonneg_iff
Ancestors0
No ancestors.