Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+ā†‘Ctrl+ā†“to navigate, Ctrl+šŸ–±ļøto focus. On Mac, use Cmdinstead of Ctrl.
/-
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 :
ā„¤: Type
ā„¤
) : ā†‘(
x: { x // 0 < x }
x
^ n) = (
x: { x // 0 < x }
x
:
K: Type ?u.2016
K
) ^ 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