chore(algebra/order/hom/basic): move positivity extension (#17758)

The positivity extension for functions instantiating `nonneg_hom_class` (e.g. the absolute value) currently lives in the file `algebra/order/hom/basic` where `nonneg_hom_class` is introduced.  This imports all of positivity (and therefore all of the theory of ordered fields and powers, much of norm_num, etc) into `algebra/order/hom/basic`, which is a lot more theory than needed.  Also, since the (apparent) only import of that file is `tactic/positivity`, it confuses the import-graph generator when the `--exclude-tactics` flag is turned on, leading to issues such as this one mentioned on the port wiki currently:
```
algebra.order.absolute_value: 'No: incorrectly marked as ready: needs algebra.hom.group'
```

Let's instead put that positivity extension in the core `tactic/positivity` file.  This requires importing `algebra/order/hom/basic` to `tactic/positivity` but it's not a heavy import since it's short and its only import `algebra/hom/group` was already imported.

Most of this PR consists of adding explicit imports to files downstream from `algebra/order/hom/basic`, when these imports were previously available as part of the big mass of positivity prerequisites.

This PR touches a frozen file (`algebra/order/hom/basic`) but only for meta code, which I believe is permissible.

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
 
 /-!

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
 

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.

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

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

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
 
 /-!

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

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

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

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