Semifield structure on the type of nonnegative elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 canonically_linear_ordered_semifield if α is a linear_ordered_field.

source

@[protected, instance]

def nonneg.has_inv {α : Type u_1} [linear_ordered_semifield α] :

has_inv {x // 0 ≤ x}

Equations

nonneg.has_inv = {inv := λ (x : {x // 0 ≤ x}), ⟨(↑x)⁻¹, _⟩}

source

@[protected, simp, norm_cast]

theorem nonneg.coe_inv {α : Type u_1} [linear_ordered_semifield α] (a : {x // 0 ≤ x}) :

↑a⁻¹ = (↑a)⁻¹

source

@[simp]

theorem nonneg.inv_mk {α : Type u_1} [linear_ordered_semifield α] {x : α} (hx : 0 ≤ x) :

⟨x, hx⟩⁻¹ = ⟨x⁻¹, _⟩

source

@[protected, instance]

def nonneg.has_div {α : Type u_1} [linear_ordered_semifield α] :

has_div {x // 0 ≤ x}

Equations

nonneg.has_div = {div := λ (x y : {x // 0 ≤ x}), ⟨↑x / ↑y, _⟩}

source

@[protected, simp, norm_cast]

theorem nonneg.coe_div {α : Type u_1} [linear_ordered_semifield α] (a b : {x // 0 ≤ x}) :

↑(a / b) = ↑a / ↑b

source

@[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, _⟩

source

@[protected, instance]

def nonneg.has_zpow {α : Type u_1} [linear_ordered_semifield α] :

has_pow {x // 0 ≤ x} ℤ

Equations

nonneg.has_zpow = {pow := λ (a : {x // 0 ≤ x}) (n : ℤ), ⟨↑a ^ n, _⟩}

source

@[protected, simp, norm_cast]

theorem nonneg.coe_zpow {α : Type u_1} [linear_ordered_semifield α] (a : {x // 0 ≤ x}) (n : ℤ) :

↑(a ^ n) = ↑a ^ n

source

@[simp]

theorem nonneg.mk_zpow {α : Type u_1} [linear_ordered_semifield α] {x : α} (hx : 0 ≤ x) (n : ℤ) :

⟨x, hx⟩ ^ n = ⟨x ^ n, _⟩

source

@[protected, instance]

def nonneg.linear_ordered_semifield {α : Type u_1} [linear_ordered_semifield α] :

linear_ordered_semifield {x // 0 ≤ x}

Equations

nonneg.linear_ordered_semifield = function.injective.linear_ordered_semifield coe nonneg.linear_ordered_semifield._proof_3 nonneg.linear_ordered_semifield._proof_4 nonneg.linear_ordered_semifield._proof_5 nonneg.linear_ordered_semifield._proof_6 nonneg.linear_ordered_semifield._proof_7 nonneg.coe_inv nonneg.coe_div nonneg.linear_ordered_semifield._proof_8 nonneg.linear_ordered_semifield._proof_9 nonneg.coe_zpow nonneg.linear_ordered_semifield._proof_10 nonneg.linear_ordered_semifield._proof_11 nonneg.linear_ordered_semifield._proof_12

source

@[protected, instance]

def nonneg.canonically_linear_ordered_semifield {α : Type u_1} [linear_ordered_field α] :

canonically_linear_ordered_semifield {x // 0 ≤ x}

Equations

nonneg.canonically_linear_ordered_semifield = {add := linear_ordered_semifield.add nonneg.linear_ordered_semifield, add_assoc := _, zero := linear_ordered_semifield.zero nonneg.linear_ordered_semifield, zero_add := _, add_zero := _, nsmul := linear_ordered_semifield.nsmul nonneg.linear_ordered_semifield, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := linear_ordered_semifield.le nonneg.linear_ordered_semifield, lt := linear_ordered_semifield.lt nonneg.linear_ordered_semifield, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := canonically_ordered_comm_semiring.bot nonneg.canonically_ordered_comm_semiring, bot_le := _, exists_add_of_le := _, le_self_add := _, mul := linear_ordered_semifield.mul nonneg.linear_ordered_semifield, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := linear_ordered_semifield.one nonneg.linear_ordered_semifield, one_mul := _, mul_one := _, nat_cast := linear_ordered_semifield.nat_cast nonneg.linear_ordered_semifield, nat_cast_zero := _, nat_cast_succ := _, npow := linear_ordered_semifield.npow nonneg.linear_ordered_semifield, npow_zero' := _, npow_succ' := _, mul_comm := _, eq_zero_or_eq_zero_of_mul_eq_zero := _, le_of_add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, le_total := _, decidable_le := linear_ordered_semifield.decidable_le nonneg.linear_ordered_semifield, decidable_eq := linear_ordered_semifield.decidable_eq nonneg.linear_ordered_semifield, decidable_lt := linear_ordered_semifield.decidable_lt nonneg.linear_ordered_semifield, max := linear_ordered_semifield.max nonneg.linear_ordered_semifield, max_def := _, min := linear_ordered_semifield.min nonneg.linear_ordered_semifield, min_def := _, inv := linear_ordered_semifield.inv nonneg.linear_ordered_semifield, div := linear_ordered_semifield.div nonneg.linear_ordered_semifield, div_eq_mul_inv := _, zpow := linear_ordered_semifield.zpow nonneg.linear_ordered_semifield, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_zero := _, mul_inv_cancel := _}

source

@[protected, instance]

def nonneg.linear_ordered_comm_group_with_zero {α : Type u_1} [linear_ordered_field α] :

linear_ordered_comm_group_with_zero {x // 0 ≤ x}

Equations

nonneg.linear_ordered_comm_group_with_zero = infer_instance