Semifield structure on the type of nonnegative elements

This file defines instances and prove some properties about the nonnegative elements Nonneg α of an arbitrary type α.

This is used to derive algebraic structures on ℝ≥0 and ℚ≥0 automatically.

theorem NNRat.cast_nonneg {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) : 0 ≤ ↑q

theorem nnqsmul_nonneg {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (q : ℚ≥0) (ha : 0 ≤ a) : 0 ≤ q • a

def Nonneg.unitsEquivPos (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] : (Nonneg R)ˣ ≃* { r : R // 0 < r }

In an ordered field, the units of the nonnegative elements are the positive elements.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Nonneg.val_unitsEquivPos_symm_apply_coe (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] (r : { r : R // 0 < r }) : ↑↑((unitsEquivPos R).symm r) = ↑r

@[simp]

theorem Nonneg.val_inv_unitsEquivPos_symm_apply_coe (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] (r : { r : R // 0 < r }) : ↑↑((unitsEquivPos R).symm r)⁻¹ = (↑r)⁻¹

@[simp]

theorem Nonneg.unitsEquivPos_apply_coe (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] (r : (Nonneg R)ˣ) : ↑((unitsEquivPos R) r) = ↑↑r

@[instance_reducible]

instance Nonneg.inv {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] : Inv (Nonneg α)

Equations

• Nonneg.inv = { inv := fun (x : Nonneg α) => ⟨(↑x)⁻¹, ⋯⟩ }

@[simp]

theorem Nonneg.coe_inv {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] (a : Nonneg α) : ↑a⁻¹ = (↑a)⁻¹

@[simp]

theorem Nonneg.inv_mk {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} (hx : 0 ≤ x) : ⟨x, hx⟩⁻¹ = ⟨x⁻¹, ⋯⟩

@[instance_reducible]

instance Nonneg.div {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] : Div (Nonneg α)

Equations

• Nonneg.div = { div := fun (x y : Nonneg α) => ⟨↑x / ↑y, ⋯⟩ }

@[simp]

theorem Nonneg.coe_div {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] (a b : Nonneg α) : ↑(a / b) = ↑a / ↑b

@[simp]

theorem Nonneg.mk_div_mk {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) : ⟨x, hx⟩ / ⟨y, hy⟩ = ⟨x / y, ⋯⟩

@[instance_reducible]

instance Nonneg.zpow {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] : Pow (Nonneg α) ℤ

Equations

• Nonneg.zpow = { pow := fun (a : Nonneg α) (n : ℤ) => ⟨↑a ^ n, ⋯⟩ }

@[simp]

theorem Nonneg.coe_zpow {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] (a : Nonneg α) (n : ℤ) : ↑(a ^ n) = ↑a ^ n

@[simp]

theorem Nonneg.mk_zpow {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] {x : α} (hx : 0 ≤ x) (n : ℤ) : ⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩

@[instance_reducible]

instance Nonneg.instNNRatCast {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] : NNRatCast (Nonneg α)

Equations

• Nonneg.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => ⟨↑q, ⋯⟩ }

@[instance_reducible]

instance Nonneg.instNNRatSMul {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] : SMul ℚ≥0 (Nonneg α)

Equations

• Nonneg.instNNRatSMul = { smul := fun (q : ℚ≥0) (a : Nonneg α) => ⟨q • ↑a, ⋯⟩ }

@[simp]

theorem Nonneg.coe_nnratCast {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) : ↑↑q = ↑q

@[simp]

theorem Nonneg.mk_nnratCast {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) : ⟨↑q, ⋯⟩ = ↑q

@[simp]

theorem Nonneg.coe_nnqsmul {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) (a : Nonneg α) : ↑(q • a) = q • ↑a

@[simp]

theorem Nonneg.mk_nnqsmul {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0) (a : α) (ha : 0 ≤ a) : ↑⟨q • a, ⋯⟩ = q • a

@[instance_reducible]

instance Nonneg.divisionSemiring {α : Type u_1} [DivisionSemiring α] [LinearOrder α] [IsStrictOrderedRing α] : DivisionSemiring (Nonneg α)

Equations

• Nonneg.divisionSemiring = Function.Injective.divisionSemiring (fun (a : { x : α // 0 ≤ x }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance Nonneg.semifield {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] : Semifield { x : α // 0 ≤ x }

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Nonneg.linearOrderedCommGroupWithZero {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] : LinearOrderedCommGroupWithZero (Nonneg α)

Equations

• One or more equations did not get rendered due to their size.