Theorems · Definition · order theory

RingPreordering.support

{R : Type u_1} → [inst : CommRing R] → (P : RingPreordering R) → [P.HasIdealSupport] → Ideal R

The support of a ring preordering P in a commutative ring R is the set of elements x in R such that both x and -x lie in P.

Defined in

Mathlib.Algebra.Order.Ring.Ordering.Defs

Cited by

9 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

CommRingRingPreordering.HasIdealSupport