# 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.
theorem NNRat.cast_nonneg {α : Type u_1} (q : ℚ≥0) :
0 q
theorem nnqsmul_nonneg {α : Type u_1} {a : α} (q : ℚ≥0) (ha : 0 a) :
0 q a
instance Nonneg.inv {α : Type u_1} :
Inv { x : α // 0 x }
Equations
• Nonneg.inv = { inv := fun (x : { x : α // 0 x }) => (x)⁻¹, }
@[simp]
theorem Nonneg.coe_inv {α : Type u_1} (a : { x : α // 0 x }) :
a⁻¹ = (a)⁻¹
@[simp]
theorem Nonneg.inv_mk {α : Type u_1} {x : α} (hx : 0 x) :
x, hx⁻¹ = x⁻¹,
instance Nonneg.div {α : Type u_1} :
Div { x : α // 0 x }
Equations
• Nonneg.div = { div := fun (x y : { x : α // 0 x }) => x / y, }
@[simp]
theorem Nonneg.coe_div {α : Type u_1} (a : { x : α // 0 x }) (b : { x : α // 0 x }) :
(a / b) = a / b
@[simp]
theorem Nonneg.mk_div_mk {α : Type u_1} {x : α} {y : α} (hx : 0 x) (hy : 0 y) :
x, hx / y, hy = x / y,
instance Nonneg.zpow {α : Type u_1} :
Pow { x : α // 0 x }
Equations
• Nonneg.zpow = { pow := fun (a : { x : α // 0 x }) (n : ) => a ^ n, }
@[simp]
theorem Nonneg.coe_zpow {α : Type u_1} (a : { x : α // 0 x }) (n : ) :
(a ^ n) = a ^ n
@[simp]
theorem Nonneg.mk_zpow {α : Type u_1} {x : α} (hx : 0 x) (n : ) :
x, hx ^ n = x ^ n,
instance Nonneg.instNNRatCast {α : Type u_1} :
NNRatCast { x : α // 0 x }
Equations
• Nonneg.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => q, }
instance Nonneg.instNNRatSMul {α : Type u_1} :
SMul ℚ≥0 { x : α // 0 x }
Equations
• Nonneg.instNNRatSMul = { smul := fun (q : ℚ≥0) (a : { x : α // 0 x }) => q a, }
@[simp]
theorem Nonneg.coe_nnratCast {α : Type u_1} (q : ℚ≥0) :
q = q
@[simp]
theorem Nonneg.mk_nnratCast {α : Type u_1} (q : ℚ≥0) :
q, = q
@[simp]
theorem Nonneg.coe_nnqsmul {α : Type u_1} (q : ℚ≥0) (a : { x : α // 0 x }) :
(q a) = q a
@[simp]
theorem Nonneg.mk_nnqsmul {α : Type u_1} (q : ℚ≥0) (a : α) (ha : 0 a) :
q a, = q a
instance Nonneg.linearOrderedSemifield {α : Type u_1} :
LinearOrderedSemifield { x : α // 0 x }
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• Nonneg.linearOrderedCommGroupWithZero = inferInstance