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

• S.toOrderedSemiring = S.toOrderedSemiring

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

• S.toStrictOrderedSemiring = S.toStrictOrderedSemiring

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

• S.toOrderedCommSemiring = S.toOrderedCommSemiring

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

• S.toStrictOrderedCommSemiring = S.toStrictOrderedCommSemiring

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

• S.toOrderedRing = S.toSubring.toOrderedRing

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

• S.toOrderedCommRing = S.toSubring.toOrderedCommRing

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

• S.toLinearOrderedSemiring = S.toLinearOrderedSemiring

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

• S.toLinearOrderedCommSemiring = S.toLinearOrderedCommSemiring

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

• S.toLinearOrderedRing = S.toSubring.toLinearOrderedRing

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

• S.toLinearOrderedCommRing = S.toSubring.toLinearOrderedCommRing