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 = OrderedSemiring.mk ⋯ ⋯ ⋯ ⋯

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

A subsemiring of a StrictOrderedSemiring is a StrictOrderedSemiring.

Equations

• SubsemiringClass.toStrictOrderedSemiring s = StrictOrderedSemiring.mk ⋯ ⋯ ⋯ ⋯ ⋯

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

A subsemiring of an OrderedCommSemiring is an OrderedCommSemiring.

Equations

• SubsemiringClass.toOrderedCommSemiring s = OrderedCommSemiring.mk ⋯

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

A subsemiring of a StrictOrderedCommSemiring is a StrictOrderedCommSemiring.

Equations

• SubsemiringClass.toStrictOrderedCommSemiring s = StrictOrderedCommSemiring.mk ⋯

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

A subsemiring of a LinearOrderedSemiring is a LinearOrderedSemiring.

Equations

• One or more equations did not get rendered due to their size.

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

A subsemiring of a LinearOrderedCommSemiring is a LinearOrderedCommSemiring.

Equations

• SubsemiringClass.toLinearOrderedCommSemiring s = LinearOrderedCommSemiring.mk ⋯ LinearOrderedSemiring.decidableLE LinearOrderedSemiring.decidableEq LinearOrderedSemiring.decidableLT ⋯ ⋯ ⋯

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

A subsemiring of an OrderedSemiring is an OrderedSemiring.

Equations

• s.toOrderedSemiring = SubsemiringClass.toOrderedSemiring s

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

A subsemiring of a StrictOrderedSemiring is a StrictOrderedSemiring.

Equations

• s.toStrictOrderedSemiring = SubsemiringClass.toStrictOrderedSemiring s

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

A subsemiring of an OrderedCommSemiring is an OrderedCommSemiring.

Equations

• s.toOrderedCommSemiring = SubsemiringClass.toOrderedCommSemiring s

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

A subsemiring of a StrictOrderedCommSemiring is a StrictOrderedCommSemiring.

Equations

• s.toStrictOrderedCommSemiring = SubsemiringClass.toStrictOrderedCommSemiring s

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

A subsemiring of a LinearOrderedSemiring is a LinearOrderedSemiring.

Equations

• s.toLinearOrderedSemiring = SubsemiringClass.toLinearOrderedSemiring s

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

A subsemiring of a LinearOrderedCommSemiring is a LinearOrderedCommSemiring.

Equations

• s.toLinearOrderedCommSemiring = SubsemiringClass.toLinearOrderedCommSemiring s

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' := ⋯ }

@[simp]

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