diff --git a/archive/oxford_invariants/2021summer/week3_p1.lean b/archive/oxford_invariants/2021summer/week3_p1.lean
index 090b4d44b0766..237a6eb375d8b 100644
--- a/archive/oxford_invariants/2021summer/week3_p1.lean
+++ b/archive/oxford_invariants/2021summer/week3_p1.lean
@@ -5,6 +5,7 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import algebra.big_operators.order
 import algebra.big_operators.ring
+import algebra.char_zero
 import data.rat.cast
 
 /-!
diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean
index ef28790279a41..8c000829e8b30 100644
--- a/src/algebra/algebra/basic.lean
+++ b/src/algebra/algebra/basic.lean
@@ -8,6 +8,7 @@ import algebra.module.ulift
 import algebra.ne_zero
 import algebra.ring.aut
 import algebra.ring.ulift
+import algebra.char_zero
 import linear_algebra.span
 import tactic.abel
 
diff --git a/src/algebra/big_operators/order.lean b/src/algebra/big_operators/order.lean
index 32c2a01fe1fac..093e4e390cac3 100644
--- a/src/algebra/big_operators/order.lean
+++ b/src/algebra/big_operators/order.lean
@@ -7,6 +7,7 @@ Authors: Johannes Hölzl
 import algebra.order.absolute_value
 import algebra.order.ring.with_top
 import algebra.big_operators.basic
+import data.fintype.card
 
 /-!
 # Results about big operators with values in an ordered algebraic structure.
diff --git a/src/algebra/order/absolute_value.lean b/src/algebra/order/absolute_value.lean
index f5d26f7b8ee3a..6571e26ced82f 100644
--- a/src/algebra/order/absolute_value.lean
+++ b/src/algebra/order/absolute_value.lean
@@ -3,7 +3,12 @@ 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.group_with_zero.units.lemmas
+import algebra.order.field.defs
 import algebra.order.hom.basic
+import algebra.order.ring.abs
+import algebra.ring.commute
+import algebra.ring.regular
 
 /-!
 # Absolute values
diff --git a/src/algebra/order/hom/basic.lean b/src/algebra/order/hom/basic.lean
index 8e2502ab1184e..4f29cd6027e46 100644
--- a/src/algebra/order/hom/basic.lean
+++ b/src/algebra/order/hom/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import tactic.positivity
+import algebra.hom.group
 
 /-!
 # Algebraic order homomorphism classes
@@ -85,14 +85,3 @@ by simpa only [div_mul_div_cancel'] using map_mul_le_mul f (a / b) (b / c)
 lemma le_map_div_add_map_div [group α] [add_comm_semigroup β] [has_le β]
   [mul_le_add_hom_class F α β] (f : F) (a b c: α) : f (a / c) ≤ f (a / b) + f (b / c) :=
 by simpa only [div_mul_div_cancel'] using map_mul_le_add f (a / b) (b / c)
-
-namespace tactic
-open positivity
-
-/-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/
-@[positivity]
-meta def positivity_map : expr → tactic strictness
-| (expr.app `(⇑%%f) `(%%a)) := nonnegative <$> mk_app ``map_nonneg [f, a]
-| _ := failed
-
-end tactic
diff --git a/src/analysis/normed/group/seminorm.lean b/src/analysis/normed/group/seminorm.lean
index a182d15fe6b0b..9ee6ab03cfe60 100644
--- a/src/analysis/normed/group/seminorm.lean
+++ b/src/analysis/normed/group/seminorm.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 María Inés de Frutos-Fernández, Yaël Dillies. All rights
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: María Inés de Frutos-Fernández, Yaël Dillies
 -/
-import algebra.order.hom.basic
+import tactic.positivity
 import data.real.nnreal
 
 /-!
diff --git a/src/combinatorics/set_family/lym.lean b/src/combinatorics/set_family/lym.lean
index 8bb5c5ba8cd9d..750963e21c261 100644
--- a/src/combinatorics/set_family/lym.lean
+++ b/src/combinatorics/set_family/lym.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Alena Gusakov, Yaël Dillies
 -/
 import algebra.big_operators.ring
+import algebra.order.field.basic
 import combinatorics.double_counting
 import combinatorics.set_family.shadow
 import data.rat.order
diff --git a/src/data/real/cau_seq.lean b/src/data/real/cau_seq.lean
index c115d2abfae8f..55206449af54e 100644
--- a/src/data/real/cau_seq.lean
+++ b/src/data/real/cau_seq.lean
@@ -3,9 +3,10 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import algebra.order.absolute_value
 import algebra.big_operators.order
+import algebra.order.absolute_value
 import algebra.order.group.min_max
+import algebra.order.field.basic
 
 /-!
 # Cauchy sequences
diff --git a/src/tactic/positivity.lean b/src/tactic/positivity.lean
index 51bf7afa13f6f..517de217a063b 100644
--- a/src/tactic/positivity.lean
+++ b/src/tactic/positivity.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Heather Macbeth, Yaël Dillies
 -/
 import tactic.norm_num
 import algebra.order.field.power
+import algebra.order.hom.basic
 
 /-! # `positivity` tactic
 
@@ -732,4 +733,10 @@ meta def positivity_finset_card : expr → tactic strictness
 | e := pp e >>= fail ∘ format.bracket "The expression `"
     "` isn't of the form `finset.card s` or `fintype.card α`"
 
+/-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/
+@[positivity]
+meta def positivity_map : expr → tactic strictness
+| (expr.app `(⇑%%f) `(%%a)) := nonnegative <$> mk_app ``map_nonneg [f, a]
+| _ := failed
+
 end tactic
diff --git a/src/topology/algebra/order/field.lean b/src/topology/algebra/order/field.lean
index 934f9c52c0404..58445c3027a37 100644
--- a/src/topology/algebra/order/field.lean
+++ b/src/topology/algebra/order/field.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Benjamin Davidson, Devon Tuma, Eric Rodriguez, Oliver Nash
 -/
 
+import tactic.positivity
 import topology.algebra.order.basic
 import topology.algebra.field