/-
Copyright (c) 2022 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module algebra.order.positive.field
! leanprover-community/mathlib commit bbeb185db4ccee8ed07dc48449414ebfa39cb821
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Algebra.Order.Positive.Ring

/-!
# Algebraic structures on the set of positive numbers

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


variable {
K: Type ?u.2
K : 
Type _: Type (?u.2+1)
Type _} [
LinearOrderedField: Type ?u.548 → Type ?u.548
LinearOrderedField 
K: Type ?u.2
K]

namespace Positive

instance 
Subtype.inv: {K : Type u_1} → [inst : LinearOrderedField K] → Inv { x // 0 < x }
Subtype.inv : 
Inv: Type ?u.14 → Type ?u.14
Inv { 
x: K
x : 
K: Type ?u.8
K // 
0: ?m.21
0 < 
x: K
x } :=
  ⟨fun 
x: ?m.161
x => ⟨
x: ?m.161
x⁻¹, 
inv_pos: ∀ {α : Type ?u.338} [inst : LinearOrderedSemifield α] {a : α}, 0 < a⁻¹ ↔ 0 < a
inv_pos.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
x: ?m.161
x.
2: ∀ {α : Sort ?u.384} {p : α → Prop} (self : Subtype p), p ↑self
2⟩⟩

@[simp]
theorem 
coe_inv: ∀ {K : Type u_1} [inst : LinearOrderedField K] (x : { x // 0 < x }), ↑x⁻¹ = (↑x)⁻¹
coe_inv (
x: { x // 0 < x }
x : { 
x: K
x : 
K: Type ?u.545
K // 
0: ?m.557
0 < 
x: K
x }) : ↑
x: { x // 0 < x }
x⁻¹ = (
x: { x // 0 < x }
x⁻¹ : 
K: Type ?u.545
K) :=
  
rfl: ∀ {α : Sort ?u.1015} {a : α}, a = a
rfl
#align positive.coe_inv 
Positive.coe_inv: ∀ {K : Type u_1} [inst : LinearOrderedField K] (x : { x // 0 < x }), ↑x⁻¹ = (↑x)⁻¹
Positive.coe_inv

instance: {K : Type u_1} → [inst : LinearOrderedField K] → Pow { x // 0 < x } ℤ
instance : 
Pow: Type ?u.1051 → Type ?u.1050 → Type (max?u.1051?u.1050)
Pow { 
x: K
x : 
K: Type ?u.1044
K // 
0: ?m.1058
0 < 
x: K
x } 
ℤ: Type
ℤ :=
  ⟨fun 
x: ?m.1202
x 
n: ?m.1205
n => ⟨(
x: ?m.1202
x: 
K: Type ?u.1044
K) ^ 
n: ?m.1205
n, 
zpow_pos_of_pos: ∀ {α : Type ?u.1456} [inst : LinearOrderedSemifield α] {a : α}, 0 < a → ∀ (n : ℤ), 0 < a ^ n
zpow_pos_of_pos 
x: ?m.1202
x.
2: ∀ {α : Sort ?u.1460} {p : α → Prop} (self : Subtype p), p ↑self
2 
_: ℤ
_⟩⟩

@[simp]
theorem 
coe_zpow: ∀ (x : { x // 0 < x }) (n : ℤ), ↑(x ^ n) = ↑x ^ n
coe_zpow (
x: { x // 0 < x }
x : { 
x: K
x : 
K: Type ?u.2016
K // 
0: ?m.2028
0 < 
x: K
x }) (
n: ℤ
n : 
ℤ: Type
ℤ) : ↑(
x: { x // 0 < x }
x ^ 
n: ℤ
n) = (
x: { x // 0 < x }
x : 
K: Type ?u.2016
K) ^ 
n: ℤ
n :=
  
rfl: ∀ {α : Sort ?u.6334} {a : α}, a = a
rfl
#align positive.coe_zpow 
Positive.coe_zpow: ∀ {K : Type u_1} [inst : LinearOrderedField K] (x : { x // 0 < x }) (n : ℤ), ↑(x ^ n) = ↑x ^ n
Positive.coe_zpow

instance: {K : Type u_1} → [inst : LinearOrderedField K] → LinearOrderedCommGroup { x // 0 < x }
instance : 
LinearOrderedCommGroup: Type ?u.6375 → Type ?u.6375
LinearOrderedCommGroup { 
x: K
x : 
K: Type ?u.6369
K // 
0: ?m.6382
0 < 
x: K
x } :=
  { 
Positive.Subtype.inv: {K : Type ?u.6518} → [inst : LinearOrderedField K] → Inv { x // 0 < x }
Positive.Subtype.inv, 
Positive.linearOrderedCancelCommMonoid: {R : Type ?u.6527} → [inst : LinearOrderedCommSemiring R] → LinearOrderedCancelCommMonoid { x // 0 < x }
Positive.linearOrderedCancelCommMonoid with
    mul_left_inv := fun 
a: ?m.6824
a => 
Subtype.ext: ∀ {α : Sort ?u.6826} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext <| 
inv_mul_cancel: ∀ {G₀ : Type ?u.6840} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ * a = 1
inv_mul_cancel 
a: ?m.6824
a.
2: ∀ {α : Sort ?u.6880} {p : α → Prop} (self : Subtype p), p ↑self
2.
ne': ∀ {α : Type ?u.6885} [inst : Preorder α] {x y : α}, x < y → y ≠ x
ne' }

end Positive