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

• {x : α // 0 ≤ x} is a CanonicallyLinearOrderedSemifield if α is a LinearOrderedField.

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

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

instance Nonneg.inv {α : Type u_1} [LinearOrderedSemifield α] : Inv { x : α // 0 ≤ x }

Equations

• Nonneg.inv = { inv := fun (x : { x : α // 0 ≤ x }) => { val := (↑x)⁻¹, property := ⋯ } }

@[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 := ⋯ }

instance Nonneg.div {α : Type u_1} [LinearOrderedSemifield α] : Div { x : α // 0 ≤ x }

Equations

• Nonneg.div = { div := fun (x y : { x : α // 0 ≤ x }) => { val := ↑x / ↑y, property := ⋯ } }

@[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 := ⋯ }

instance Nonneg.zpow {α : Type u_1} [LinearOrderedSemifield α] : Pow { x : α // 0 ≤ x } ℤ

Equations

• Nonneg.zpow = { pow := fun (a : { x : α // 0 ≤ x }) (n : ℤ) => { val := ↑a ^ n, property := ⋯ } }

@[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 := ⋯ }

instance Nonneg.instNNRatCast {α : Type u_1} [LinearOrderedSemifield α] : NNRatCast { x : α // 0 ≤ x }

Equations

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

instance Nonneg.instNNRatSMul {α : Type u_1} [LinearOrderedSemifield α] : SMul ℚ≥0 { x : α // 0 ≤ x }

Equations

• Nonneg.instNNRatSMul = { smul := fun (q : ℚ≥0) (a : { x : α // 0 ≤ x }) => { val := q • ↑a, property := ⋯ } }

@[simp]

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

@[simp]

theorem Nonneg.mk_nnratCast {α : Type u_1} [LinearOrderedSemifield α] (q : ℚ≥0) : { val := ↑q, property := ⋯ } = ↑q

@[simp]

theorem Nonneg.coe_nnqsmul {α : Type u_1} [LinearOrderedSemifield α] (q : ℚ≥0) (a : { x : α // 0 ≤ x }) : ↑(q • a) = q • ↑a

@[simp]

theorem Nonneg.mk_nnqsmul {α : Type u_1} [LinearOrderedSemifield α] (q : ℚ≥0) (a : α) (ha : 0 ≤ a) : ↑{ val := q • a, property := ⋯ } = q • a

instance Nonneg.linearOrderedSemifield {α : Type u_1} [LinearOrderedSemifield α] : LinearOrderedSemifield { x : α // 0 ≤ x }

Equations

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

instance Nonneg.canonicallyLinearOrderedSemifield {α : Type u_1} [LinearOrderedField α] : CanonicallyLinearOrderedSemifield { x : α // 0 ≤ x }

Equations

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

instance Nonneg.linearOrderedCommGroupWithZero {α : Type u_1} [LinearOrderedField α] : LinearOrderedCommGroupWithZero { x : α // 0 ≤ x }

Equations

• Nonneg.linearOrderedCommGroupWithZero = inferInstance