# mathlib3documentation

algebra.order.nonneg.field

# Semifield structure on the type of nonnegative elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 canonically_linear_ordered_semifield if α is a linear_ordered_field.
@[protected, instance]
def nonneg.has_inv {α : Type u_1}  :
has_inv {x // 0 x}
Equations
@[protected, simp, norm_cast]
theorem nonneg.coe_inv {α : Type u_1} (a : {x // 0 x}) :
@[simp]
theorem nonneg.inv_mk {α : Type u_1} {x : α} (hx : 0 x) :
x, hx⟩⁻¹ = x⁻¹, _⟩
@[protected, instance]
def nonneg.has_div {α : Type u_1}  :
has_div {x // 0 x}
Equations
@[protected, simp, norm_cast]
theorem nonneg.coe_div {α : Type u_1} (a 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, _⟩
@[protected, instance]
def nonneg.has_zpow {α : Type u_1}  :
has_pow {x // 0 x}
Equations
@[protected, simp, norm_cast]
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, _⟩
@[protected, instance]
Equations
• nonneg.linear_ordered_semifield = nonneg.linear_ordered_semifield._proof_3 nonneg.linear_ordered_semifield._proof_4 nonneg.linear_ordered_semifield._proof_5 nonneg.linear_ordered_semifield._proof_6 nonneg.linear_ordered_semifield._proof_7 nonneg.coe_inv nonneg.coe_div nonneg.linear_ordered_semifield._proof_8 nonneg.linear_ordered_semifield._proof_9 nonneg.coe_zpow nonneg.linear_ordered_semifield._proof_10 nonneg.linear_ordered_semifield._proof_11 nonneg.linear_ordered_semifield._proof_12
@[protected, instance]
Equations
@[protected, instance]
Equations