Ordered instances for SubsemiringClass and Subsemiring.

instance SubsemiringClass.toOrderedSemiring {R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [OrderedSemiring R] [SubsemiringClass S R] : OrderedSemiring ↥s

A subsemiring of an OrderedSemiring is an OrderedSemiring.

Equations

• SubsemiringClass.toOrderedSemiring s = Function.Injective.orderedSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SubsemiringClass.toStrictOrderedSemiring {R : Type u_1} {S : Type u_2} (s : S) [StrictOrderedSemiring R] [SetLike S R] [SubsemiringClass S R] : StrictOrderedSemiring ↥s

A subsemiring of a StrictOrderedSemiring is a StrictOrderedSemiring.

Equations

• SubsemiringClass.toStrictOrderedSemiring s = Function.Injective.strictOrderedSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SubsemiringClass.toOrderedCommSemiring {R : Type u_1} {S : Type u_2} (s : S) [OrderedCommSemiring R] [SetLike S R] [SubsemiringClass S R] : OrderedCommSemiring ↥s

A subsemiring of an OrderedCommSemiring is an OrderedCommSemiring.

Equations

• SubsemiringClass.toOrderedCommSemiring s = Function.Injective.orderedCommSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SubsemiringClass.toStrictOrderedCommSemiring {R : Type u_1} {S : Type u_2} (s : S) [StrictOrderedCommSemiring R] [SetLike S R] [SubsemiringClass S R] : StrictOrderedCommSemiring ↥s

A subsemiring of a StrictOrderedCommSemiring is a StrictOrderedCommSemiring.

Equations

• SubsemiringClass.toStrictOrderedCommSemiring s = Function.Injective.strictOrderedCommSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SubsemiringClass.toLinearOrderedSemiring {R : Type u_1} {S : Type u_2} (s : S) [LinearOrderedSemiring R] [SetLike S R] [SubsemiringClass S R] : LinearOrderedSemiring ↥s

A subsemiring of a LinearOrderedSemiring is a LinearOrderedSemiring.

Equations

• SubsemiringClass.toLinearOrderedSemiring s = Function.Injective.linearOrderedSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SubsemiringClass.toLinearOrderedCommSemiring {R : Type u_1} {S : Type u_2} (s : S) [LinearOrderedCommSemiring R] [SetLike S R] [SubsemiringClass S R] : LinearOrderedCommSemiring ↥s

A subsemiring of a LinearOrderedCommSemiring is a LinearOrderedCommSemiring.

Equations

• SubsemiringClass.toLinearOrderedCommSemiring s = Function.Injective.linearOrderedCommSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Subsemiring.toOrderedSemiring {R : Type u_1} [OrderedSemiring R] (s : Subsemiring R) : OrderedSemiring ↥s

A subsemiring of an OrderedSemiring is an OrderedSemiring.

Equations

• Subsemiring.toOrderedSemiring s = Function.Injective.orderedSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Subsemiring.toStrictOrderedSemiring {R : Type u_1} [StrictOrderedSemiring R] (s : Subsemiring R) : StrictOrderedSemiring ↥s

A subsemiring of a StrictOrderedSemiring is a StrictOrderedSemiring.

Equations

• Subsemiring.toStrictOrderedSemiring s = Function.Injective.strictOrderedSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Subsemiring.toOrderedCommSemiring {R : Type u_1} [OrderedCommSemiring R] (s : Subsemiring R) : OrderedCommSemiring ↥s

A subsemiring of an OrderedCommSemiring is an OrderedCommSemiring.

Equations

• Subsemiring.toOrderedCommSemiring s = Function.Injective.orderedCommSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Subsemiring.toStrictOrderedCommSemiring {R : Type u_1} [StrictOrderedCommSemiring R] (s : Subsemiring R) : StrictOrderedCommSemiring ↥s

A subsemiring of a StrictOrderedCommSemiring is a StrictOrderedCommSemiring.

Equations

• Subsemiring.toStrictOrderedCommSemiring s = Function.Injective.strictOrderedCommSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Subsemiring.toLinearOrderedSemiring {R : Type u_1} [LinearOrderedSemiring R] (s : Subsemiring R) : LinearOrderedSemiring ↥s

A subsemiring of a LinearOrderedSemiring is a LinearOrderedSemiring.

Equations

• Subsemiring.toLinearOrderedSemiring s = Function.Injective.linearOrderedSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Subsemiring.toLinearOrderedCommSemiring {R : Type u_1} [LinearOrderedCommSemiring R] (s : Subsemiring R) : LinearOrderedCommSemiring ↥s

A subsemiring of a LinearOrderedCommSemiring is a LinearOrderedCommSemiring.

Equations

• Subsemiring.toLinearOrderedCommSemiring s = Function.Injective.linearOrderedCommSemiring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Subsemiring.nonneg_carrier (R : Type u_2) [OrderedSemiring R] : ↑(Subsemiring.nonneg R) = Set.Ici 0

def Subsemiring.nonneg (R : Type u_2) [OrderedSemiring R] : Subsemiring R

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

Equations

• Subsemiring.nonneg R = { toSubmonoid := { toSubsemigroup := { carrier := Set.Ici 0, mul_mem' := ⋯ }, one_mem' := ⋯ }, add_mem' := ⋯, zero_mem' := ⋯ }