Order instances on subalgebras

instance Subalgebra.toOrderedSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [OrderedSemiring A] [Algebra R A] (S : Subalgebra R A) : OrderedSemiring ↥S

Equations

• Subalgebra.toOrderedSemiring S = Subsemiring.toOrderedSemiring S.toSubsemiring

instance Subalgebra.toStrictOrderedSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [StrictOrderedSemiring A] [Algebra R A] (S : Subalgebra R A) : StrictOrderedSemiring ↥S

Equations

• Subalgebra.toStrictOrderedSemiring S = Subsemiring.toStrictOrderedSemiring S.toSubsemiring

instance Subalgebra.toOrderedCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [OrderedCommSemiring A] [Algebra R A] (S : Subalgebra R A) : OrderedCommSemiring ↥S

Equations

• Subalgebra.toOrderedCommSemiring S = Subsemiring.toOrderedCommSemiring S.toSubsemiring

instance Subalgebra.toStrictOrderedCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [StrictOrderedCommSemiring A] [Algebra R A] (S : Subalgebra R A) : StrictOrderedCommSemiring ↥S

Equations

• Subalgebra.toStrictOrderedCommSemiring S = Subsemiring.toStrictOrderedCommSemiring S.toSubsemiring

instance Subalgebra.toOrderedRing {R : Type u_1} {A : Type u_2} [CommRing R] [OrderedRing A] [Algebra R A] (S : Subalgebra R A) : OrderedRing ↥S

Equations

• Subalgebra.toOrderedRing S = Subring.toOrderedRing (Subalgebra.toSubring S)

instance Subalgebra.toOrderedCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [OrderedCommRing A] [Algebra R A] (S : Subalgebra R A) : OrderedCommRing ↥S

Equations

• Subalgebra.toOrderedCommRing S = Subring.toOrderedCommRing (Subalgebra.toSubring S)

instance Subalgebra.toLinearOrderedSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [LinearOrderedSemiring A] [Algebra R A] (S : Subalgebra R A) : LinearOrderedSemiring ↥S

Equations

• Subalgebra.toLinearOrderedSemiring S = Subsemiring.toLinearOrderedSemiring S.toSubsemiring

instance Subalgebra.toLinearOrderedCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [LinearOrderedCommSemiring A] [Algebra R A] (S : Subalgebra R A) : LinearOrderedCommSemiring ↥S

Equations

• Subalgebra.toLinearOrderedCommSemiring S = Subsemiring.toLinearOrderedCommSemiring S.toSubsemiring

instance Subalgebra.toLinearOrderedRing {R : Type u_1} {A : Type u_2} [CommRing R] [LinearOrderedRing A] [Algebra R A] (S : Subalgebra R A) : LinearOrderedRing ↥S

Equations

• Subalgebra.toLinearOrderedRing S = Subring.toLinearOrderedRing (Subalgebra.toSubring S)

instance Subalgebra.toLinearOrderedCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [LinearOrderedCommRing A] [Algebra R A] (S : Subalgebra R A) : LinearOrderedCommRing ↥S

Equations

• Subalgebra.toLinearOrderedCommRing S = Subring.toLinearOrderedCommRing (Subalgebra.toSubring S)