Algebraic structures on the set of positive numbers #

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

In this file we prove that the set of positive elements of a linear ordered field is a linear ordered commutative group.

source

@[protected, instance]

def positive.subtype.has_inv {K : Type u_1} [linear_ordered_field K] :

has_inv {x // 0 < x}

Equations

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

source

@[simp]

theorem positive.coe_inv {K : Type u_1} [linear_ordered_field K] (x : {x // 0 < x}) :

↑x⁻¹ = (↑x)⁻¹

source

@[protected, instance]

def positive.int.has_pow {K : Type u_1} [linear_ordered_field K] :

has_pow {x // 0 < x} ℤ

Equations

positive.int.has_pow = {pow := λ (x : {x // 0 < x}) (n : ℤ), ⟨↑x ^ n, _⟩}

source

@[simp]

theorem positive.coe_zpow {K : Type u_1} [linear_ordered_field K] (x : {x // 0 < x}) (n : ℤ) :

↑(x ^ n) = ↑x ^ n

source

@[protected, instance]

def positive.subtype.linear_ordered_comm_group {K : Type u_1} [linear_ordered_field K] :

linear_ordered_comm_group {x // 0 < x}

Equations

positive.subtype.linear_ordered_comm_group = {mul := linear_ordered_cancel_comm_monoid.mul positive.subtype.linear_ordered_cancel_comm_monoid, mul_assoc := _, one := linear_ordered_cancel_comm_monoid.one positive.subtype.linear_ordered_cancel_comm_monoid, one_mul := _, mul_one := _, npow := linear_ordered_cancel_comm_monoid.npow positive.subtype.linear_ordered_cancel_comm_monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv positive.subtype.has_inv, div := ordered_comm_group.div._default linear_ordered_cancel_comm_monoid.mul positive.subtype.linear_ordered_comm_group._proof_6 linear_ordered_cancel_comm_monoid.one positive.subtype.linear_ordered_comm_group._proof_7 positive.subtype.linear_ordered_comm_group._proof_8 linear_ordered_cancel_comm_monoid.npow positive.subtype.linear_ordered_comm_group._proof_9 positive.subtype.linear_ordered_comm_group._proof_10 has_inv.inv, div_eq_mul_inv := _, zpow := ordered_comm_group.zpow._default linear_ordered_cancel_comm_monoid.mul positive.subtype.linear_ordered_comm_group._proof_12 linear_ordered_cancel_comm_monoid.one positive.subtype.linear_ordered_comm_group._proof_13 positive.subtype.linear_ordered_comm_group._proof_14 linear_ordered_cancel_comm_monoid.npow positive.subtype.linear_ordered_comm_group._proof_15 positive.subtype.linear_ordered_comm_group._proof_16 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := linear_ordered_cancel_comm_monoid.le positive.subtype.linear_ordered_cancel_comm_monoid, lt := linear_ordered_cancel_comm_monoid.lt positive.subtype.linear_ordered_cancel_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_total := _, decidable_le := linear_ordered_cancel_comm_monoid.decidable_le positive.subtype.linear_ordered_cancel_comm_monoid, decidable_eq := linear_ordered_cancel_comm_monoid.decidable_eq positive.subtype.linear_ordered_cancel_comm_monoid, decidable_lt := linear_ordered_cancel_comm_monoid.decidable_lt positive.subtype.linear_ordered_cancel_comm_monoid, max := linear_ordered_cancel_comm_monoid.max positive.subtype.linear_ordered_cancel_comm_monoid, max_def := _, min := linear_ordered_cancel_comm_monoid.min positive.subtype.linear_ordered_cancel_comm_monoid, min_def := _}