Structures · Algebra
IsStrictOrderedRing
A strict ordered semiring is a nontrivial semiring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.
- Defined in
- Mathlib.Algebra.Order.Ring.Defs
- Shape
- One type argument
Extends5
Extended by0
Nothing extends this class yet.
Concrete types that are instances14
- Int
- Nat
- Real
- Rat
- NNReal
- Filter.Germ
- NNRat
- Hyperreal
- Zsqrtd
- ZNum
- ArchimedeanClass.FiniteElement
- Num
- Subtype
- Lex
How is a type an instance?
Loading the hierarchy index…
Assumed by2,754
- Orientation
- CauSeq
- SameRay
- IsCauSeq
- half_pos
- CauSeq.Completion.Cauchy
- Convexity.ConvexSpace.sConvexComb
- CauSeq.const
- AffineSubspace.SOppSide
- AffineSubspace.SSameSide
- Int.cast_abs
- Convexity.convexCombPair
- AffineSubspace.WSameSide
- Convexity.iConvexComb
- AffineSubspace.WOppSide
- CauSeq.LimZero
- HahnSeries.ofPowerSeries
- Convexity.StdSimplex.map
- abs_div
- half_lt_self
- Module.Basis.ofZLatticeBasis
- Convexity.IsConvexSet
- CauSeq.lim
- abs_inv
- one_half_pos
- Filter.Tendsto.const_mul_atTop
- Module.Ray
- Module.Basis.orientation
- exists_rat_btwn
- exists_nat_gt
- Orientation.map
- RootPairing.posRootForm
- rayOfNeZero
- Convexity.convexHull
- tendsto_pow_atTop_atTop_of_one_lt
- Filter.Tendsto.inv_tendsto_atTop
- Convexity.StdSimplex.duple
- Convexity.IsStarConvexSet
- Convex.ordConnected
- Convexity.StdSimplex.single
- tendsto_inv_atTop_zero
- Nat.floor_natCast
- SameRay.congr_simp
- tendsto_pow_atTop_nhds_zero_of_lt_one
- Convexity.StdSimplex.weights_map
- Matrix.GLPos
- exists_pow_lt_of_lt_one
- sq_le_sq
- CauSeq.equiv_lim
- ArchimedeanClass.addValuation