Structures · Algebra
RingPreordering.IsOrdering
An ordering O on a ring R is a preordering such that
1. O contains either x or -x for each x in R and
2. the support of O is a prime ideal.
- Defined in
- Mathlib.Algebra.Order.Ring.Ordering.Defs
- Shape
- One type argument
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…