chore(algebra/order/field): don't import finiteness hierarchy (#17350)

This problem was just introduced in #16971. Hopefully we can all be careful about not adding heavy imports to fundamental files. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Nov 5, 2022 · ef0ef21 · ef0ef21
1 parent e9b8651
commit ef0ef21
Show file tree

Hide file tree

Showing 14 changed files with 42 additions and 28 deletions.
diff --git a/src/algebra/continued_fractions/computation/basic.lean b/src/algebra/continued_fractions/computation/basic.lean
@@ -5,7 +5,7 @@ Authors: Kevin Kappelmann
 -/
 import algebra.order.floor
 import algebra.continued_fractions.basic
-import algebra.order.field
+import algebra.order.field.basic
 /-!
 # Computable Continued Fractions
 

diff --git a/src/algebra/order/absolute_value.lean b/src/algebra/order/absolute_value.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Anne Baanen
 -/
-import algebra.order.field
+import algebra.order.field.basic
 import algebra.order.hom.basic
 
 /-!

diff --git a/src/algebra/order/field.lean → src/algebra/order/field/basic.lean b/src/algebra/order/field.lean → src/algebra/order/field/basic.lean
@@ -3,9 +3,8 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
-import algebra.order.field_defs
-import algebra.order.with_zero
-import data.fintype.basic
+import algebra.order.field.defs
+import algebra.group_with_zero.power
 
 /-!
 # Linear ordered (semi)fields
@@ -635,19 +634,6 @@ lemma is_glb.mul_right {s : set α} (ha : 0 ≤ a) (hs : is_glb s b) :
   is_glb ((λ b, b * a) '' s) (b * a) :=
 by simpa [mul_comm] using hs.mul_left ha
 
-lemma pi.exists_forall_pos_add_lt [has_exists_add_of_le α] [finite ι] {x y : ι → α}
-  (h : ∀ i, x i < y i) : ∃ ε, 0 < ε ∧ ∀ i, x i + ε < y i :=
-begin
-  casesI nonempty_fintype ι,
-  casesI is_empty_or_nonempty ι,
-  { exact ⟨1, zero_lt_one, is_empty_elim⟩ },
-  choose ε hε hxε using λ i, exists_pos_add_of_lt' (h i),
-  obtain rfl : x + ε = y := funext hxε,
-  have hε : 0 < finset.univ.inf' finset.univ_nonempty ε := (finset.lt_inf'_iff _).2 (λ i _, hε _),
-  exact ⟨_, half_pos hε, λ i, add_lt_add_left ((half_lt_self hε).trans_le $ finset.inf'_le _ $
-    finset.mem_univ _) _⟩,
-end
-
 end linear_ordered_semifield
 
 section

diff --git a/src/algebra/order/field_defs.lean → src/algebra/order/field/defs.lean b/src/algebra/order/field_defs.lean → src/algebra/order/field/defs.lean
@@ -21,7 +21,7 @@ A linear ordered (semi)field is a (semi)field equipped with a linear order such
 
 ## Implementation details
 
-For olean caching reasons, this file is separate to the main file, algebra.order.field.
+For olean caching reasons, this file is separate to the main file, `algebra.order.field.basic`.
 The lemmata are instead located there.
 
 -/

diff --git a/src/algebra/order/field/pi.lean b/src/algebra/order/field/pi.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2014 Robert Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import algebra.order.field.basic
+import data.fintype.basic
+
+/-!
+# Lemmas about (finite domain) functions into fields.
+
+We split this from `algebra.order.field.basic` to avoid importing the finiteness hierarchy there.
+-/
+
+variables {α ι : Type*} [linear_ordered_semifield α]
+
+lemma pi.exists_forall_pos_add_lt [has_exists_add_of_le α] [finite ι] {x y : ι → α}
+  (h : ∀ i, x i < y i) : ∃ ε, 0 < ε ∧ ∀ i, x i + ε < y i :=
+begin
+  casesI nonempty_fintype ι,
+  casesI is_empty_or_nonempty ι,
+  { exact ⟨1, zero_lt_one, is_empty_elim⟩ },
+  choose ε hε hxε using λ i, exists_pos_add_of_lt' (h i),
+  obtain rfl : x + ε = y := funext hxε,
+  have hε : 0 < finset.univ.inf' finset.univ_nonempty ε := (finset.lt_inf'_iff _).2 (λ i _, hε _),
+  exact ⟨_, half_pos hε, λ i, add_lt_add_left ((half_lt_self hε).trans_le $ finset.inf'_le _ $
+    finset.mem_univ _) _⟩,
+end
diff --git a/src/algebra/order/positive/field.lean b/src/algebra/order/positive/field.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import algebra.order.field
+import algebra.order.field.basic
 import algebra.order.positive.ring
 
 /-!

diff --git a/src/algebra/order/smul.lean b/src/algebra/order/smul.lean
@@ -5,7 +5,7 @@ Authors: Frédéric Dupuis
 -/
 import algebra.module.pi
 import algebra.module.prod
-import algebra.order.field
+import algebra.order.field.basic
 import algebra.order.pi
 import data.set.pointwise.basic
 import tactic.positivity

diff --git a/src/analysis/special_functions/bernstein.lean b/src/analysis/special_functions/bernstein.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import algebra.order.field
+import algebra.order.field.basic
 import ring_theory.polynomial.bernstein
 import topology.continuous_function.polynomial
 

diff --git a/src/analysis/specific_limits/normed.lean b/src/analysis/specific_limits/normed.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker, Sébastien Gouëzel, Yury G. Kudryashov, Dylan MacKenzie, Patrick Massot
 -/
-import algebra.order.field
+import algebra.order.field.basic
 import analysis.asymptotics.asymptotics
 import analysis.specific_limits.basic
 

diff --git a/src/data/nat/cast_field.lean b/src/data/nat/cast_field.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yaël Dillies, Patrick Stevens
 -/
-import algebra.order.field
+import algebra.order.field.basic
 import data.nat.cast
 
 /-!

diff --git a/src/data/nat/choose/bounds.lean b/src/data/nat/choose/bounds.lean
@@ -5,7 +5,7 @@ Authors: Yaël Dillies, Eric Rodriguez
 -/
 
 import algebra.group_power.lemmas
-import algebra.order.field
+import algebra.order.field.basic
 import data.nat.cast
 import data.nat.choose.basic
 

diff --git a/src/data/rat/order.lean b/src/data/rat/order.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
-import algebra.order.field
+import algebra.order.field.basic
 import data.rat.basic
 
 /-!

diff --git a/src/data/set/intervals/image_preimage.lean b/src/data/set/intervals/image_preimage.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov, Patrick Massot
 -/
 import data.set.pointwise.basic
-import algebra.order.field
+import algebra.order.field.basic
 
 /-!
 # (Pre)images of intervals

diff --git a/src/order/filter/at_top_bot.lean b/src/order/filter/at_top_bot.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jeremy Avigad, Yury Kudryashov, Patrick Massot
 -/
-import algebra.order.field
+import algebra.order.field.basic
 import data.finset.preimage
 import data.set.intervals.disjoint
 import order.filter.bases