Skip to content

Commit c6727ac

Browse files
YaelDilliesYaelDillies
committed
chore: Move basic ordered field lemmas
These lemmas are needed to define the semifield structure on `NNRat`, hence I am repurposing `Algebra.Order.Field.Defs` from avoiding a timeout (which I believe was solved long ago) to avoiding to import random stuff in the definition of the semifield structure on `NNRat` (although this PR doesn't actually reduce imports there, it will be in a later PR). Reduce the diff of #11203
1 parent c9a0699 commit c6727ac

File tree

2 files changed

+62
-92
lines changed

2 files changed

+62
-92
lines changed

‎Mathlib/Algebra/Order/Field/Basic.lean‎

Lines changed: 0 additions & 84 deletions
Original file line numberDiff line numberDiff line change
@@ -40,90 +40,6 @@ def OrderIso.mulRight₀ (a : α) (ha : 0 < a) : α ≃o α :=
4040
#align order_iso.mul_right₀_symm_apply OrderIso.mulRight₀_symm_apply
4141
#align order_iso.mul_right₀_apply OrderIso.mulRight₀_apply
4242

43-
/-!
44-
### Lemmas about pos, nonneg, nonpos, neg
45-
-/
46-
47-
48-
@[simp]
49-
theorem inv_pos : 0 < a⁻¹ ↔ 0 < a :=
50-
suffices ∀ a : α, 0 < a → 0 < a⁻¹ from ⟨fun h => inv_inv a ▸ this _ h, this a⟩
51-
fun a ha => flip lt_of_mul_lt_mul_left ha.le <| by simp [ne_of_gt ha, zero_lt_one]
52-
#align inv_pos inv_pos
53-
54-
alias ⟨_, inv_pos_of_pos⟩ := inv_pos
55-
#align inv_pos_of_pos inv_pos_of_pos
56-
57-
@[simp]
58-
theorem inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a := by
59-
simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]
60-
#align inv_nonneg inv_nonneg
61-
62-
alias ⟨_, inv_nonneg_of_nonneg⟩ := inv_nonneg
63-
#align inv_nonneg_of_nonneg inv_nonneg_of_nonneg
64-
65-
@[simp]
66-
theorem inv_lt_zero : a⁻¹ < 0 ↔ a < 0 := by simp only [← not_le, inv_nonneg]
67-
#align inv_lt_zero inv_lt_zero
68-
69-
@[simp]
70-
theorem inv_nonpos : a⁻¹ ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, inv_pos]
71-
#align inv_nonpos inv_nonpos
72-
73-
theorem one_div_pos : 0 < 1 / a ↔ 0 < a :=
74-
inv_eq_one_div a ▸ inv_pos
75-
#align one_div_pos one_div_pos
76-
77-
theorem one_div_neg : 1 / a < 0 ↔ a < 0 :=
78-
inv_eq_one_div a ▸ inv_lt_zero
79-
#align one_div_neg one_div_neg
80-
81-
theorem one_div_nonneg : 0 ≤ 1 / a ↔ 0 ≤ a :=
82-
inv_eq_one_div a ▸ inv_nonneg
83-
#align one_div_nonneg one_div_nonneg
84-
85-
theorem one_div_nonpos : 1 / a ≤ 0 ↔ a ≤ 0 :=
86-
inv_eq_one_div a ▸ inv_nonpos
87-
#align one_div_nonpos one_div_nonpos
88-
89-
theorem div_pos (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by
90-
rw [div_eq_mul_inv]
91-
exact mul_pos ha (inv_pos.2 hb)
92-
#align div_pos div_pos
93-
94-
theorem div_nonneg (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b := by
95-
rw [div_eq_mul_inv]
96-
exact mul_nonneg ha (inv_nonneg.2 hb)
97-
#align div_nonneg div_nonneg
98-
99-
theorem div_nonpos_of_nonpos_of_nonneg (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0 := by
100-
rw [div_eq_mul_inv]
101-
exact mul_nonpos_of_nonpos_of_nonneg ha (inv_nonneg.2 hb)
102-
#align div_nonpos_of_nonpos_of_nonneg div_nonpos_of_nonpos_of_nonneg
103-
104-
theorem div_nonpos_of_nonneg_of_nonpos (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0 := by
105-
rw [div_eq_mul_inv]
106-
exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)
107-
#align div_nonpos_of_nonneg_of_nonpos div_nonpos_of_nonneg_of_nonpos
108-
109-
theorem zpow_nonneg (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
110-
| (n : ℕ) => by
111-
rw [zpow_coe_nat]
112-
exact pow_nonneg ha _
113-
| -(n + 1 : ℕ) => by
114-
rw [zpow_neg, inv_nonneg, zpow_coe_nat]
115-
exact pow_nonneg ha _
116-
#align zpow_nonneg zpow_nonneg
117-
118-
theorem zpow_pos_of_pos (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n
119-
| (n : ℕ) => by
120-
rw [zpow_coe_nat]
121-
exact pow_pos ha _
122-
| -(n + 1 : ℕ) => by
123-
rw [zpow_neg, inv_pos, zpow_coe_nat]
124-
exact pow_pos ha _
125-
#align zpow_pos_of_pos zpow_pos_of_pos
126-
12743
/-!
12844
### Relating one division with another term.
12945
-/

‎Mathlib/Algebra/Order/Field/Defs.lean‎

Lines changed: 62 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
55
-/
66
import Mathlib.Algebra.Field.Defs
7+
import Mathlib.Algebra.GroupWithZero.Units.Basic
78
import Mathlib.Algebra.Order.Ring.Defs
89

910
#align_import algebra.order.field.defs from "leanprover-community/mathlib"@"655994e298904d7e5bbd1e18c95defd7b543eb94"
@@ -20,14 +21,10 @@ A linear ordered (semi)field is a (semi)field equipped with a linear order such
2021
2122
* `LinearOrderedSemifield`: Typeclass for linear order semifields.
2223
* `LinearOrderedField`: Typeclass for linear ordered fields.
23-
24-
## Implementation details
25-
26-
For olean caching reasons, this file is separate to the main file,
27-
`Mathlib.Algebra.Order.Field.Basic`. The lemmata are instead located there.
28-
2924
-/
3025

26+
-- Guard against import creep.
27+
assert_not_exists MonoidHom
3128

3229
variable {α : Type*}
3330

@@ -45,5 +42,62 @@ instance (priority := 100) LinearOrderedField.toLinearOrderedSemifield [LinearOr
4542
{ LinearOrderedRing.toLinearOrderedSemiring, ‹LinearOrderedField α› with }
4643
#align linear_ordered_field.to_linear_ordered_semifield LinearOrderedField.toLinearOrderedSemifield
4744

48-
-- Guard against import creep.
49-
assert_not_exists MonoidHom
45+
variable [LinearOrderedSemifield α] {a b : α}
46+
47+
@[simp] lemma inv_pos : 0 < a⁻¹ ↔ 0 < a :=
48+
suffices ∀ a : α, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
49+
fun a ha ↦ flip lt_of_mul_lt_mul_left ha.le <| by simp [ne_of_gt ha, zero_lt_one]
50+
#align inv_pos inv_pos
51+
52+
alias ⟨_, inv_pos_of_pos⟩ := inv_pos
53+
#align inv_pos_of_pos inv_pos_of_pos
54+
55+
@[simp] lemma inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a := by simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]
56+
#align inv_nonneg inv_nonneg
57+
58+
alias ⟨_, inv_nonneg_of_nonneg⟩ := inv_nonneg
59+
#align inv_nonneg_of_nonneg inv_nonneg_of_nonneg
60+
61+
@[simp] lemma inv_lt_zero : a⁻¹ < 0 ↔ a < 0 := by simp only [← not_le, inv_nonneg]
62+
#align inv_lt_zero inv_lt_zero
63+
64+
@[simp] lemma inv_nonpos : a⁻¹ ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, inv_pos]
65+
#align inv_nonpos inv_nonpos
66+
67+
lemma one_div_pos : 0 < 1 / a ↔ 0 < a := inv_eq_one_div a ▸ inv_pos
68+
#align one_div_pos one_div_pos
69+
70+
lemma one_div_neg : 1 / a < 0 ↔ a < 0 := inv_eq_one_div a ▸ inv_lt_zero
71+
#align one_div_neg one_div_neg
72+
73+
lemma one_div_nonneg : 0 ≤ 1 / a ↔ 0 ≤ a := inv_eq_one_div a ▸ inv_nonneg
74+
#align one_div_nonneg one_div_nonneg
75+
76+
lemma one_div_nonpos : 1 / a ≤ 0 ↔ a ≤ 0 := inv_eq_one_div a ▸ inv_nonpos
77+
#align one_div_nonpos one_div_nonpos
78+
79+
lemma div_pos (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by
80+
rw [div_eq_mul_inv]; exact mul_pos ha (inv_pos.2 hb)
81+
#align div_pos div_pos
82+
83+
lemma div_nonneg (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b := by
84+
rw [div_eq_mul_inv]; exact mul_nonneg ha (inv_nonneg.2 hb)
85+
#align div_nonneg div_nonneg
86+
87+
lemma div_nonpos_of_nonpos_of_nonneg (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0 := by
88+
rw [div_eq_mul_inv]; exact mul_nonpos_of_nonpos_of_nonneg ha (inv_nonneg.2 hb)
89+
#align div_nonpos_of_nonpos_of_nonneg div_nonpos_of_nonpos_of_nonneg
90+
91+
lemma div_nonpos_of_nonneg_of_nonpos (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0 := by
92+
rw [div_eq_mul_inv]; exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)
93+
#align div_nonpos_of_nonneg_of_nonpos div_nonpos_of_nonneg_of_nonpos
94+
95+
lemma zpow_nonneg (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
96+
| (n : ℕ) => by rw [zpow_coe_nat]; exact pow_nonneg ha _
97+
| -(n + 1 : ℕ) => by rw [zpow_neg, inv_nonneg, zpow_coe_nat]; exact pow_nonneg ha _
98+
#align zpow_nonneg zpow_nonneg
99+
100+
lemma zpow_pos_of_pos (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n
101+
| (n : ℕ) => by rw [zpow_coe_nat]; exact pow_pos ha _
102+
| -(n + 1 : ℕ) => by rw [zpow_neg, inv_pos, zpow_coe_nat]; exact pow_pos ha _
103+
#align zpow_pos_of_pos zpow_pos_of_pos

0 commit comments

Comments
 (0)