mathlib documentation

algebra.order.nonneg.field

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 #

@[protected, instance]
def nonneg.has_inv {α : Type u_1} [linear_ordered_semifield α] :
has_inv {x // 0 x}
Equations
@[protected, simp, norm_cast]
theorem nonneg.coe_inv {α : Type u_1} [linear_ordered_semifield α] (a : {x // 0 x}) :
@[simp]
theorem nonneg.inv_mk {α : Type u_1} [linear_ordered_semifield α] {x : α} (hx : 0 x) :
x, hx⟩⁻¹ = x⁻¹, _⟩
@[protected, instance]
def nonneg.has_div {α : Type u_1} [linear_ordered_semifield α] :
has_div {x // 0 x}
Equations
@[protected, simp, norm_cast]
theorem nonneg.coe_div {α : Type u_1} [linear_ordered_semifield α] (a b : {x // 0 x}) :
(a / b) = a / b
@[simp]
theorem nonneg.mk_div_mk {α : Type u_1} [linear_ordered_semifield α] {x y : α} (hx : 0 x) (hy : 0 y) :
x, hx⟩ / y, hy⟩ = x / y, _⟩
@[protected, instance]
def nonneg.has_zpow {α : Type u_1} [linear_ordered_semifield α] :
has_pow {x // 0 x}
Equations
@[protected, simp, norm_cast]
theorem nonneg.coe_zpow {α : Type u_1} [linear_ordered_semifield α] (a : {x // 0 x}) (n : ) :
(a ^ n) = a ^ n
@[simp]
theorem nonneg.mk_zpow {α : Type u_1} [linear_ordered_semifield α] {x : α} (hx : 0 x) (n : ) :
x, hx⟩ ^ n = x ^ n, _⟩
@[protected, instance]
Equations
@[protected, instance]
Equations

Floor #

@[protected, instance]
@[protected, instance]
Equations
@[norm_cast]
theorem nonneg.nat_floor_coe {α : Type u_1} [ordered_semiring α] [floor_semiring α] (a : {r // 0 r}) :
@[norm_cast]
theorem nonneg.nat_ceil_coe {α : Type u_1} [ordered_semiring α] [floor_semiring α] (a : {r // 0 r}) :