Skip to content

Commit 842f262

Browse files
YaelDilliesutensil
YaelDillies
authored and
utensil
committed
chore: Move basic ordered field lemmas (#11503)
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 183415a commit 842f262

File tree

20 files changed

+91
-112
lines changed

20 files changed

+91
-112
lines changed

‎Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Kevin Kappelmann
55
-/
66
import Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
77
import Mathlib.Algebra.ContinuedFractions.TerminatedStable
8-
import Mathlib.Algebra.Order.Field.Basic
98
import Mathlib.Tactic.FieldSimp
109
import Mathlib.Tactic.Ring
1110

‎Mathlib/Algebra/GeomSum.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,9 @@ Authors: Neil Strickland
66
import Mathlib.Algebra.BigOperators.Order
77
import Mathlib.Algebra.BigOperators.Ring
88
import Mathlib.Algebra.BigOperators.Intervals
9-
import Mathlib.Tactic.Abel
9+
import Mathlib.Algebra.Order.Field.Basic
1010
import Mathlib.Data.Nat.Parity
11+
import Mathlib.Tactic.Abel
1112

1213
#align_import algebra.geom_sum from "leanprover-community/mathlib"@"f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c"
1314

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

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

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

‎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

‎Mathlib/Algebra/Order/Module/Pointwise.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,9 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6-
import Mathlib.Data.Set.Pointwise.SMul
76
import Mathlib.Algebra.Order.Module.Defs
7+
import Mathlib.Data.Set.Pointwise.SMul
8+
import Mathlib.Order.Bounds.OrderIso
89

910
/-!
1011
# Bounds on scalar multiplication of set

‎Mathlib/Algebra/Order/Monovary.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies
55
-/
6+
import Mathlib.Algebra.Order.Field.Basic
67
import Mathlib.Algebra.Order.Group.Defs
78
import Mathlib.Algebra.Order.Group.Instances
89
import Mathlib.Algebra.Order.Module.OrderedSMul

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Floris van Doorn
55
-/
6-
import Mathlib.Algebra.Order.Field.Basic
76
import Mathlib.Algebra.Order.Field.Canonical.Defs
87
import Mathlib.Algebra.Order.Field.InjSurj
98
import Mathlib.Algebra.Order.Nonneg.Ring

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov
55
-/
6-
import Mathlib.Algebra.Order.Field.Basic
6+
import Mathlib.Algebra.Order.Field.Defs
77
import Mathlib.Algebra.Order.Positive.Ring
88

99
#align_import algebra.order.positive.field from "leanprover-community/mathlib"@"bbeb185db4ccee8ed07dc48449414ebfa39cb821"

‎Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,8 @@ Authors: Yaël Dillies, Vladimir Ivanov
55
-/
66
import Mathlib.Algebra.BigOperators.Intervals
77
import Mathlib.Algebra.BigOperators.Order
8-
import Mathlib.Algebra.BigOperators.Ring
8+
import Mathlib.Algebra.Order.Field.Basic
99
import Mathlib.Data.Finset.Sups
10-
import Mathlib.Order.Hom.Lattice
1110
import Mathlib.Tactic.FieldSimp
1211
import Mathlib.Tactic.Ring
1312

‎Mathlib/Combinatorics/SimpleGraph/Density.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@ Copyright (c) 2022 Yaël Dillies, Bhavik Mehta. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yaël Dillies, Bhavik Mehta
55
-/
6+
import Mathlib.Algebra.Order.Field.Basic
67
import Mathlib.Combinatorics.SimpleGraph.Basic
7-
import Mathlib.Order.Partition.Finpartition
88
import Mathlib.Data.Rat.Cast.Order
9-
import Mathlib.Tactic.Ring
10-
import Mathlib.Tactic.NormNum
9+
import Mathlib.Order.Partition.Finpartition
1110
import Mathlib.Tactic.GCongr
1211
import Mathlib.Tactic.Positivity
12+
import Mathlib.Tactic.Ring
1313

1414
#align_import combinatorics.simple_graph.density from "leanprover-community/mathlib"@"a4ec43f53b0bd44c697bcc3f5a62edd56f269ef1"
1515

0 commit comments

Comments
 (0)