Structures · Algebra
StarOrderedRing
An ordered \-ring is a \-ring with a partial order such that the nonnegative elements
constitute precisely the AddSubmonoid generated by elements of the form star s * s.
If you are working with a NonUnitalRing and not a NonUnitalSemiring, it may be more
convenient to declare instances using StarOrderedRing.of_nonneg_iff.
- Defined in
- Mathlib.Algebra.Order.Star.Basic
- Shape
- One type argument · adds le_iff
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances13
- Int
- Nat
- Real
- Rat
- NNReal
- ContinuousLinearMap
- CStarMatrix
- NNRat
- Unitization
- ContinuousMapZero
- Prod
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by652
- CFC.sqrt
- CFC.abs
- IsSelfAdjoint.of_nonneg
- LE.le.isSelfAdjoint
- star_mul_self_nonneg
- CFC.conjSqrt
- CFC.sqrt_nonneg
- CFC.sqrt_mul_sqrt_self
- cfcₙ_nnreal_eq_real
- cfc_nnreal_eq_real
- LE.le.star_eq
- CFC.sqrt_eq_iff
- CFC.sqrt_eq_nnrpow
- Unitization.inr_le_iff
- CFC.sqrt.congr_simp
- Unitization.inr_nonneg_iff
- CFC.rpow_zero
- CFC.sqrt_eq_rpow
- CFC.rpow_def
- IsSelfAdjoint.le_algebraMap_norm_self
- CFC.rpow
- cfcₙ_nonneg
- CStarAlgebra.isStrictlyPositive_TFAE
- CStarAlgebra.norm_le_norm_of_nonneg_of_le
- cfc_le_iff
- star_left_conjugate_nonneg
- CFC.nnrpow_one
- star_left_conjugate_le_conjugate
- CStarAlgebra.nonneg_TFAE
- star_le_star_iff
- CFC.abs.congr_simp
- CFC.nnrpow
- CFC.abs_mul_abs
- IsStarProjection.nonneg
- selfAdjoint.unitarySelfAddISMul
- CFC.rpow_rpow
- CFC.nnrpow_eq_rpow
- CStarAlgebra.norm_le_one_iff_of_nonneg
- StarOrderedRing.le_iff
- CFC.sqrt_eq_cfc
- mul_star_self_nonneg
- CStarAlgebra.norm_le_iff_le_algebraMap
- CFC.negPart_nonneg
- IsGreatest.nnnorm_cfcₙ_nnreal
- star_lt_star_iff
- CFC.posPart_nonneg
- CFC.nnrpow_nnrpow
- IsGreatest.nnnorm_cfc_nnreal
- nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
- CFC.sqrt_mul_self
Ancestors0
No ancestors.