Structures · Algebra
IsOrderedRing
An ordered semiring is a semiring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.
- Defined in
- Mathlib.Algebra.Order.Ring.Defs
- Shape
- One type argument
Extends4
Extended by0
Nothing extends this class yet.
Concrete types that are instances18
- Real
- NNReal
- ENNReal
- Filter.Germ
- ENat
- ArchimedeanClass.FiniteResidueField
- SetSemiring
- FractionalIdeal
- Cardinal
- AlgebraicGeometry.Scheme.IdealSheafData
- Subtype
- Prod
- MulOpposite
- Lex
- AddOpposite
- WithTop
- WithBot
- Submodule
How is a type an instance?
Loading the hierarchy index…
Assumed by927
- PointedCone
- Nat.cast_pos
- Nat.cast_nonneg
- abs_mul
- Even.pow_nonneg
- abs_one
- ProperCone
- tendsto_natCast_atTop_atTop
- PointedCone.dual
- ArchimedeanClass.stdPart
- HahnEmbedding.Partial
- ArchimedeanClass.FiniteElement
- abs_pow
- Nat.abs_cast
- FiniteArchimedeanClass.ball
- doublyStochastic
- PointedCone.ofSubmodule
- HahnEmbedding.ArchimedeanStrata.stratum
- Int.fract_lt_one
- exists_nat_ge
- Matrix.colStochastic
- PointedCone.map
- Matrix.rowStochastic
- stdSimplex.map
- Int.fract_nonneg
- ArchimedeanClass.FiniteResidueField
- ProperCone.dual
- Int.floor_intCast
- Filter.tendsto_pow_atTop
- HahnEmbedding.Partial.eval
- PointedCone.IsFaceOf.mem_of_smul_add_mem
- Wbtw.symm
- stdSimplex.vertex
- Nat.abs_ofNat
- Filter.Tendsto.atTop_mul_atTop₀
- PointedCone.hull
- PointedCone.DualFG
- wbtw_comm
- HahnEmbedding.Seed.baseEmbedding
- HahnEmbedding.Seed.toArchimedeanStrata
- Sbtw.symm
- Int.ceil_intCast
- PointedCone.lineal
- FiniteArchimedeanClass.closedBall
- PointedCone.IsFaceOf.le
- PointedCone.toConvexCone
- ProperCone.toPointedCone
- PointedCone.comap
- HahnEmbedding.Partial.evalCoeff
- Int.ceil_add_intCast