chore(*): more import reduction (#3421)

Another import reduction PR. (This is by hand, not just removing transitive imports.)

Mostly this one is from staring at `leanproject import-graph --to data.polynomial.basic` and wondering about weird edges in the graph.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/big_operators.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 
 import algebra.opposites
+import algebra.group.anti_hom
 import data.finset.intervals
 import data.finset.fold
 import data.finset.powerset

src/algebra/polynomial/big_operators.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jalex Stark.
 -/
 import algebra.polynomial.basic
+import tactic.linarith
+
 open polynomial finset
 
 /-!

src/combinatorics/composition.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import data.fintype.card
 import data.finset.sort
+import tactic.omega
 
 /-!
 # Compositions

src/data/fintype/card.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro
 -/
 import data.fintype.basic
-import data.nat.choose
+import algebra.big_operators
 
 /-!
 Results about "big operations" over a `fintype`, and consequent

src/data/int/sqrt.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import data.nat.sqrt
-import data.int.basic
 
 namespace int
 

src/data/nat/digits.lean

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import data.int.modeq
-import data.fintype.card
-import tactic.ring
 import tactic.interval_cases
+import tactic.linarith
 
 /-!
 # Digits of a natural number

src/data/polynomial/ring_division.lean

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 import data.polynomial.div
-
+import tactic.omega
 
 /-!
 # Theory of univariate polynomials

src/data/rat/basic.lean

@@ -3,11 +3,8 @@ 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 data.int.sqrt
 import data.equiv.encodable.basic
-import algebra.group
 import algebra.euclidean_domain
-import algebra.ordered_field
 
 /-!
 # Basics for the Rational Numbers

src/data/rat/order.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import data.rat.basic
+
 /-!
 # Order for Rational Numbers
 
@@ -222,20 +223,4 @@ begin
     rw [int.nat_abs_of_nonneg hq, num_denom] }
 end
 
-section sqrt
-
-@[pp_nodot] def sqrt (q : ℚ) : ℚ := rat.mk (int.sqrt q.num) (nat.sqrt q.denom)
-
-theorem sqrt_eq (q : ℚ) : rat.sqrt (q*q) = abs q :=
-by rw [sqrt, mul_self_num, mul_self_denom, int.sqrt_eq, nat.sqrt_eq, abs_def]
-
-theorem exists_mul_self (x : ℚ) : (∃ q, q * q = x) ↔ rat.sqrt x * rat.sqrt x = x :=
-⟨λ ⟨n, hn⟩, by rw [← hn, sqrt_eq, abs_mul_abs_self],
-λ h, ⟨rat.sqrt x, h⟩⟩
-
-theorem sqrt_nonneg (q : ℚ) : 0 ≤ rat.sqrt q :=
-nonneg_iff_zero_le.1 $ (mk_nonneg _ $ int.coe_nat_pos.2 $
-nat.pos_of_ne_zero $ λ H, nat.pos_iff_ne_zero.1 q.pos $ nat.sqrt_eq_zero.1 H).2 trivial
-
-end sqrt
 end rat

src/data/rat/sqrt.lean

@@ -0,0 +1,32 @@
+/-
+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 data.rat.order
+import data.int.sqrt
+/-!
+# Square root on rational numbers
+
+This file defines the square root function on rational numbers, `rat.sqrt` and proves several theorems about it.
+
+-/
+namespace rat
+
+/-- Square root function on rational numbers, defined by taking the (integer) square root of the
+numerator and the square root (on natural numbers) of the denominator. -/
+@[pp_nodot] def sqrt (q : ℚ) : ℚ := rat.mk (int.sqrt q.num) (nat.sqrt q.denom)
+
+theorem sqrt_eq (q : ℚ) : rat.sqrt (q*q) = abs q :=
+by rw [sqrt, mul_self_num, mul_self_denom, int.sqrt_eq, nat.sqrt_eq, abs_def]
+
+theorem exists_mul_self (x : ℚ) : (∃ q, q * q = x) ↔ rat.sqrt x * rat.sqrt x = x :=
+⟨λ ⟨n, hn⟩, by rw [← hn, sqrt_eq, abs_mul_abs_self],
+λ h, ⟨rat.sqrt x, h⟩⟩
+
+theorem sqrt_nonneg (q : ℚ) : 0 ≤ rat.sqrt q :=
+nonneg_iff_zero_le.1 $ (mk_nonneg _ $ int.coe_nat_pos.2 $
+nat.pos_of_ne_zero $ λ H, nat.pos_iff_ne_zero.1 q.pos $ nat.sqrt_eq_zero.1 H).2 trivial
+
+end rat

src/data/real/irrational.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Yury Kudryashov.
 -/
 import data.real.basic
+import data.rat.sqrt
 import algebra.gcd_domain
 import ring_theory.multiplicity
 /-!

src/group_theory/perm/sign.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes
 -/
 import data.fintype.basic
 import data.finset.sort
+import algebra.group.conj
 import algebra.big_operators
 
 universes u v

src/group_theory/subgroup.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying
 -/
 import group_theory.submonoid
+import algebra.group.conj
 
 /-!
 # Subgroups

src/tactic/norm_num.lean

@@ -5,7 +5,6 @@ Authors: Simon Hudon, Mario Carneiro
 -/
 import data.rat.cast
 import data.rat.meta_defs
-import tactic.doc_commands
 
 /-!
 # `norm_num`