From f16343dc2063e3b0987dbc505575cb950371c9af Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 11 Feb 2023 20:43:59 +0000
Subject: [PATCH] feat: port Algebra.Order.Nonneg.Field (#2200)

---
 Mathlib.lean                            |   1 +
 Mathlib/Algebra/Order/Nonneg/Field.lean | 133 ++++++++++++++++++++++++
 2 files changed, 134 insertions(+)
 create mode 100644 Mathlib/Algebra/Order/Nonneg/Field.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 1f991efb53d76..65e3fb8bb12a5 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -154,6 +154,7 @@ import Mathlib.Algebra.Order.Monoid.Units
 import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Algebra.Order.Monoid.WithZero.Basic
 import Mathlib.Algebra.Order.Monoid.WithZero.Defs
+import Mathlib.Algebra.Order.Nonneg.Field
 import Mathlib.Algebra.Order.Nonneg.Ring
 import Mathlib.Algebra.Order.Pi
 import Mathlib.Algebra.Order.Pointwise
diff --git a/Mathlib/Algebra/Order/Nonneg/Field.lean b/Mathlib/Algebra/Order/Nonneg/Field.lean
new file mode 100644
index 0000000000000..437b6cac4d02e
--- /dev/null
+++ b/Mathlib/Algebra/Order/Nonneg/Field.lean
@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2021 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+! This file was ported from Lean 3 source module algebra.order.nonneg.field
+! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Order.Archimedean
+import Mathlib.Algebra.Order.Nonneg.Ring
+import Mathlib.Algebra.Order.Field.InjSurj
+import Mathlib.Algebra.Order.Field.Canonical.Defs
+
+/-!
+# 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`.
+-/
+
+
+open Set
+
+variable {α : Type _}
+
+namespace Nonneg
+
+section LinearOrderedSemifield
+
+variable [LinearOrderedSemifield α] {x y : α}
+
+instance inv : Inv { x : α // 0 ≤ x } :=
+  ⟨fun x => ⟨x⁻¹, inv_nonneg.2 x.2⟩⟩
+#align nonneg.has_inv Nonneg.inv
+
+@[simp, norm_cast]
+protected theorem coe_inv (a : { x : α // 0 ≤ x }) : ((a⁻¹ : { x : α // 0 ≤ x }) : α) = (a : α)⁻¹ :=
+  rfl
+#align nonneg.coe_inv Nonneg.coe_inv
+
+@[simp]
+theorem inv_mk (hx : 0 ≤ x) : (⟨x, hx⟩ : { x : α // 0 ≤ x })⁻¹ = ⟨x⁻¹, inv_nonneg.2 hx⟩ :=
+  rfl
+#align nonneg.inv_mk Nonneg.inv_mk
+
+instance hasDiv : Div { x : α // 0 ≤ x } :=
+  ⟨fun x y => ⟨x / y, div_nonneg x.2 y.2⟩⟩
+#align nonneg.has_div Nonneg.hasDiv
+
+@[simp, norm_cast]
+protected theorem coe_div (a b : { x : α // 0 ≤ x }) : ((a / b : { x : α // 0 ≤ x }) : α) = a / b :=
+  rfl
+#align nonneg.coe_div Nonneg.coe_div
+
+@[simp]
+theorem mk_div_mk (hx : 0 ≤ x) (hy : 0 ≤ y) :
+    (⟨x, hx⟩ : { x : α // 0 ≤ x }) / ⟨y, hy⟩ = ⟨x / y, div_nonneg hx hy⟩ :=
+  rfl
+#align nonneg.mk_div_mk Nonneg.mk_div_mk
+
+instance hasZpow : Pow { x : α // 0 ≤ x } ℤ :=
+  ⟨fun a n => ⟨(a : α) ^ n, zpow_nonneg a.2 _⟩⟩
+#align nonneg.has_zpow Nonneg.hasZpow
+
+@[simp, norm_cast]
+protected theorem coe_zpow (a : { x : α // 0 ≤ x }) (n : ℤ) :
+    ((a ^ n : { x : α // 0 ≤ x }) : α) = (a : α) ^ n :=
+  rfl
+#align nonneg.coe_zpow Nonneg.coe_zpow
+
+@[simp]
+theorem mk_zpow (hx : 0 ≤ x) (n : ℤ) :
+    (⟨x, hx⟩ : { x : α // 0 ≤ x }) ^ n = ⟨x ^ n, zpow_nonneg hx n⟩ :=
+  rfl
+#align nonneg.mk_zpow Nonneg.mk_zpow
+
+instance linearOrderedSemifield : LinearOrderedSemifield { x : α // 0 ≤ x } :=
+  Subtype.coe_injective.linearOrderedSemifield _ Nonneg.coe_zero Nonneg.coe_one Nonneg.coe_add
+    Nonneg.coe_mul Nonneg.coe_inv Nonneg.coe_div (fun _ _ => rfl) Nonneg.coe_pow Nonneg.coe_zpow
+    Nonneg.coe_nat_cast (fun _ _ => rfl) fun _ _ => rfl
+#align nonneg.linear_ordered_semifield Nonneg.linearOrderedSemifield
+
+end LinearOrderedSemifield
+
+instance canonicallyLinearOrderedSemifield [LinearOrderedField α] :
+    CanonicallyLinearOrderedSemifield { x : α // 0 ≤ x } :=
+  { Nonneg.linearOrderedSemifield, Nonneg.canonicallyOrderedCommSemiring with }
+#align nonneg.canonically_linear_ordered_semifield Nonneg.canonicallyLinearOrderedSemifield
+
+instance linearOrderedCommGroupWithZero [LinearOrderedField α] :
+    LinearOrderedCommGroupWithZero { x : α // 0 ≤ x } :=
+  inferInstance
+#align nonneg.linear_ordered_comm_group_with_zero Nonneg.linearOrderedCommGroupWithZero
+
+/-! ### Floor -/
+
+
+instance archimedean [OrderedAddCommMonoid α] [Archimedean α] : Archimedean { x : α // 0 ≤ x } :=
+  ⟨fun x y hy =>
+    let ⟨n, hr⟩ := Archimedean.arch (x : α) (hy : (0 : α) < y)
+    ⟨n, show (x : α) ≤ (n • y : { x : α // 0 ≤ x }) by simp [*, -nsmul_eq_mul, nsmul_coe]⟩⟩
+#align nonneg.archimedean Nonneg.archimedean
+
+instance floorSemiring [OrderedSemiring α] [FloorSemiring α] :
+    FloorSemiring { r : α // 0 ≤ r } where
+  floor a := ⌊(a : α)⌋₊
+  ceil a := ⌈(a : α)⌉₊
+  floor_of_neg ha := FloorSemiring.floor_of_neg ha
+  gc_floor ha := FloorSemiring.gc_floor (Subtype.coe_le_coe.2 ha)
+  gc_ceil a n := FloorSemiring.gc_ceil (a : α) n
+#align nonneg.floor_semiring Nonneg.floorSemiring
+
+@[norm_cast]
+theorem nat_floor_coe [OrderedSemiring α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) :
+    ⌊(a : α)⌋₊ = ⌊a⌋₊ :=
+  rfl
+#align nonneg.nat_floor_coe Nonneg.nat_floor_coe
+
+@[norm_cast]
+theorem nat_ceil_coe [OrderedSemiring α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) :
+    ⌈(a : α)⌉₊ = ⌈a⌉₊ :=
+  rfl
+#align nonneg.nat_ceil_coe Nonneg.nat_ceil_coe
+
+end Nonneg