Ordered instances for SubsemiringClass and Subsemiring.

instance SubsemiringClass.toIsOrderedRing {R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [Semiring R] [PartialOrder R] [IsOrderedRing R] [SubsemiringClass S R] : IsOrderedRing ↥s

A subsemiring of an ordered semiring is an ordered semiring.

instance SubsemiringClass.toIsStrictOrderedRing {R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [SubsemiringClass S R] : IsStrictOrderedRing ↥s

A subsemiring of a strict ordered semiring is a strict ordered semiring.

instance Subsemiring.toIsOrderedRing {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] (s : Subsemiring R) : IsOrderedRing ↥s

A subsemiring of an ordered semiring is an ordered semiring.

instance Subsemiring.toIsStrictOrderedRing {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (s : Subsemiring R) : IsStrictOrderedRing ↥s

A subsemiring of a strict ordered semiring is a strict ordered semiring.

def Subsemiring.nonneg (R : Type u_1) [Semiring R] [PartialOrder R] [IsOrderedRing R] : Subsemiring R

The set of nonnegative elements in an ordered semiring, as a subsemiring.

Equations

• Subsemiring.nonneg R = { carrier := (AddSubmonoid.nonneg R).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Subsemiring.coe_nonneg (R : Type u_1) [Semiring R] [PartialOrder R] [IsOrderedRing R] : ↑(nonneg R) = (AddSubmonoid.nonneg R).carrier

@[simp]

theorem Subsemiring.mem_nonneg {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {x : R} : x ∈ nonneg R ↔ 0 ≤ x

@[simp]

theorem Subsemiring.nonneg_toAddSubmonoid (R : Type u_1) [Semiring R] [PartialOrder R] [IsOrderedRing R] : (nonneg R).toAddSubmonoid = AddSubmonoid.nonneg R