Documentation

Mathlib.Algebra.Ring.Subring.Order

Subrings of ordered rings #

We study subrings of ordered rings and prove their basic properties.

Main definitions and results #

@[instance 75]
instance SubringClass.toOrderedRing {R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [OrderedRing R] [SubringClass S R] :

A subring of an OrderedRing is an OrderedRing.

Equations
@[instance 75]
instance SubringClass.toOrderedCommRing {R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [OrderedCommRing R] [SubringClass S R] :

A subring of an OrderedCommRing is an OrderedCommRing.

Equations

The inclusion S → R of a subring, as an ordered ring homomorphism.

Equations
Instances For