Documentation

Mathlib.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 #

instance Nonneg.inv {α : Type u_1} [LinearOrderedSemifield α] :
Inv { x // 0 x }
Equations
  • Nonneg.inv = { inv := fun x => { val := (x)⁻¹, property := (_ : 0 (x)⁻¹) } }
@[simp]
theorem Nonneg.coe_inv {α : Type u_1} [LinearOrderedSemifield α] (a : { x // 0 x }) :
a⁻¹ = (a)⁻¹
@[simp]
theorem Nonneg.inv_mk {α : Type u_1} [LinearOrderedSemifield α] {x : α} (hx : 0 x) :
{ val := x, property := hx }⁻¹ = { val := x⁻¹, property := (_ : 0 x⁻¹) }
instance Nonneg.div {α : Type u_1} [LinearOrderedSemifield α] :
Div { x // 0 x }
Equations
  • Nonneg.div = { div := fun x y => { val := x / y, property := (_ : 0 x / y) } }
@[simp]
theorem Nonneg.coe_div {α : Type u_1} [LinearOrderedSemifield α] (a : { x // 0 x }) (b : { x // 0 x }) :
↑(a / b) = a / b
@[simp]
theorem Nonneg.mk_div_mk {α : Type u_1} [LinearOrderedSemifield α] {x : α} {y : α} (hx : 0 x) (hy : 0 y) :
{ val := x, property := hx } / { val := y, property := hy } = { val := x / y, property := (_ : 0 x / y) }
instance Nonneg.zpow {α : Type u_1} [LinearOrderedSemifield α] :
Pow { x // 0 x }
Equations
  • Nonneg.zpow = { pow := fun a n => { val := a ^ n, property := (_ : 0 a ^ n) } }
@[simp]
theorem Nonneg.coe_zpow {α : Type u_1} [LinearOrderedSemifield α] (a : { x // 0 x }) (n : ) :
↑(a ^ n) = a ^ n
@[simp]
theorem Nonneg.mk_zpow {α : Type u_1} [LinearOrderedSemifield α] {x : α} (hx : 0 x) (n : ) :
{ val := x, property := hx } ^ n = { val := x ^ n, property := (_ : 0 x ^ n) }
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Nonneg.linearOrderedCommGroupWithZero = inferInstance