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 { x : R // x ∈ 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} [SetLike S R] (s : S) [StrictOrderedSemiring R] [SubsemiringClass S R] : StrictOrderedSemiring { x : R // x ∈ 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} [SetLike S R] (s : S) [OrderedCommSemiring R] [SubsemiringClass S R] : OrderedCommSemiring { x : R // x ∈ 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} [SetLike S R] (s : S) [StrictOrderedCommSemiring R] [SubsemiringClass S R] : StrictOrderedCommSemiring { x : R // x ∈ 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} [SetLike S R] (s : S) [LinearOrderedSemiring R] [SubsemiringClass S R] : LinearOrderedSemiring { x : R // x ∈ 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} [SetLike S R] (s : S) [LinearOrderedCommSemiring R] [SubsemiringClass S R] : LinearOrderedCommSemiring { x : R // x ∈ 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 { x : R // x ∈ s }

A subsemiring of an OrderedSemiring is an OrderedSemiring.

Equations

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

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

A subsemiring of a StrictOrderedSemiring is a StrictOrderedSemiring.

Equations

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

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

A subsemiring of an OrderedCommSemiring is an OrderedCommSemiring.

Equations

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

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

A subsemiring of a StrictOrderedCommSemiring is a StrictOrderedCommSemiring.

Equations

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

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

A subsemiring of a LinearOrderedSemiring is a LinearOrderedSemiring.

Equations

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

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

A subsemiring of a LinearOrderedCommSemiring is a LinearOrderedCommSemiring.

Equations

• s.toLinearOrderedCommSemiring = 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 = { carrier := Set.Ici 0, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }