Theorems · Definition · field theory

Nonneg.unitsEquivPos

(R : Type u_2) →
  [inst : DivisionSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] → [PosMulReflectLT R] → { r // 0 ≤ r }ˣ ≃* { r // 0 < r }

In an ordered field, the units of the nonnegative elements are the positive elements.

Defined in

Mathlib.Algebra.Order.Nonneg.Field

Cited by

4 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionSemiringPartialOrderIsStrictOrderedRingPosMulReflectLT