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 #

theorem NNRat.cast_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) :
0 q
theorem nnqsmul_nonneg {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (q : ℚ≥0) (ha : 0 a) :
0 q a
instance Nonneg.inv {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
Inv { x : α // 0 x }
Equations
    @[simp]
    theorem Nonneg.coe_inv {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (a : { x : α // 0 x }) :
    a⁻¹ = (↑a)⁻¹
    @[simp]
    theorem Nonneg.inv_mk {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} (hx : 0 x) :
    instance Nonneg.div {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
    Div { x : α // 0 x }
    Equations
      @[simp]
      theorem Nonneg.coe_div {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (a b : { x : α // 0 x }) :
      ↑(a / b) = a / b
      @[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,
      instance Nonneg.zpow {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
      Pow { x : α // 0 x }
      Equations
        @[simp]
        theorem Nonneg.coe_zpow {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (a : { x : α // 0 x }) (n : ) :
        ↑(a ^ n) = a ^ n
        @[simp]
        theorem Nonneg.mk_zpow {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} (hx : 0 x) (n : ) :
        x, hx ^ n = x ^ n,
        instance Nonneg.instNNRatCast {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
        NNRatCast { x : α // 0 x }
        Equations
          instance Nonneg.instNNRatSMul {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
          SMul ℚ≥0 { x : α // 0 x }
          Equations
            @[simp]
            theorem Nonneg.coe_nnratCast {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) :
            q = q
            @[simp]
            theorem Nonneg.mk_nnratCast {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) :
            q, = q
            @[simp]
            theorem Nonneg.coe_nnqsmul {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) (a : { x : α // 0 x }) :
            ↑(q a) = q a
            @[simp]
            theorem Nonneg.mk_nnqsmul {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) (a : α) (ha : 0 a) :
            q a, = q a
            instance Nonneg.semifield {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] :
            Semifield { x : α // 0 x }
            Equations