# Semifield structure on the type of nonnegative elements #

This file defines instances and prove some properties about the nonnegative elements `{x : α // 0 ≤ x}` of an arbitrary type `α`.

This is used to derive algebraic structures on `ℝ≥0` and `ℚ≥0` automatically.

## Main declarations #

- `{x : α // 0 ≤ x}` is a `CanonicallyLinearOrderedSemifield` if `α` is a `LinearOrderedField`.

source
theorem NNRat.cast_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) :
0 ≤ ↑q
source
theorem nnqsmul_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (q : ℚ≥0) (ha : 0 ≤ a) :
0 ≤ q • a
source
def Nonneg.unitsEquivPos (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] :
{ r : R // 0 ≤ r }ˣ ≃* { r : R // 0 < r }

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Nonneg.val_inv_unitsEquivPos_symm_apply_coe (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] (r : { r : R // 0 < r }) :
↑↑((unitsEquivPos R).symm r)⁻¹ = (↑r)⁻¹
source
@[simp]
theorem Nonneg.val_unitsEquivPos_symm_apply_coe (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] (r : { r : R // 0 < r }) :
↑↑((unitsEquivPos R).symm r) = ↑r
source
@[simp]
theorem Nonneg.unitsEquivPos_apply_coe (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] (r : { r : R // 0 ≤ r }ˣ) :
↑((unitsEquivPos R) r) = ↑↑r
source
instance Nonneg.inv {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
Inv { x : α // 0 ≤ x }
Equations

- Nonneg.inv = { inv := fun (x : { x : α // 0 ≤ x }) => ⟨(↑x)⁻¹, ⋯⟩ }

source
@[simp]
theorem Nonneg.coe_inv {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (a : { x : α // 0 ≤ x }) :
↑a⁻¹ = (↑a)⁻¹
source
@[simp]
theorem Nonneg.inv_mk {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} (hx : 0 ≤ x) :
⟨x, hx⟩⁻¹ = ⟨x⁻¹, ⋯⟩
source
instance Nonneg.div {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
Div { x : α // 0 ≤ x }
Equations

- Nonneg.div = { div := fun (x y : { x : α // 0 ≤ x }) => ⟨↑x / ↑y, ⋯⟩ }

source
@[simp]
theorem Nonneg.coe_div {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (a b : { x : α // 0 ≤ x }) :
↑(a / b) = ↑a / ↑b
source
@[simp]
theorem Nonneg.mk_div_mk {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) :
⟨x, hx⟩ / ⟨y, hy⟩ = ⟨x / y, ⋯⟩
source
instance Nonneg.zpow {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
Pow { x : α // 0 ≤ x } ℤ
Equations

- Nonneg.zpow = { pow := fun (a : { x : α // 0 ≤ x }) (n : ℤ) => ⟨↑a ^ n, ⋯⟩ }

source
@[simp]
theorem Nonneg.coe_zpow {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (a : { x : α // 0 ≤ x }) (n : ℤ) :
↑(a ^ n) = ↑a ^ n
source
@[simp]
theorem Nonneg.mk_zpow {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} (hx : 0 ≤ x) (n : ℤ) :
⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩
source
instance Nonneg.instNNRatCast {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
NNRatCast { x : α // 0 ≤ x }
Equations

- Nonneg.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => ⟨↑q, ⋯⟩ }

source
instance Nonneg.instNNRatSMul {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
SMul ℚ≥0 { x : α // 0 ≤ x }
Equations

- Nonneg.instNNRatSMul = { smul := fun (q : ℚ≥0) (a : { x : α // 0 ≤ x }) => ⟨q • ↑a, ⋯⟩ }

source
@[simp]
theorem Nonneg.coe_nnratCast {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) :
↑↑q = ↑q
source
@[simp]
theorem Nonneg.mk_nnratCast {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) :
⟨↑q, ⋯⟩ = ↑q
source
@[simp]
theorem Nonneg.coe_nnqsmul {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) (a : { x : α // 0 ≤ x }) :
↑(q • a) = q • ↑a
source
@[simp]
theorem Nonneg.mk_nnqsmul {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) (a : α) (ha : 0 ≤ a) :
↑⟨q • a, ⋯⟩ = q • a
source
instance Nonneg.semifield {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
Semifield { x : α // 0 ≤ x }
Equations

- One or more equations did not get rendered due to their size.

source
instance Nonneg.linearOrderedCommGroupWithZero {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] :
LinearOrderedCommGroupWithZero { x : α // 0 ≤ x }
Equations

- Nonneg.linearOrderedCommGroupWithZero = CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero