chore: move NormalizedGCDMonoid ℕ to reduce imports (#12341)

Previously `Mathlib.GroupTheory.Perm.Fin` knew about `LinearMap` for no good reason, because it relied on `Mathlib.RingTheory.Int.Basic` for some basic things, but that file also has heavy imports.

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

Mathlib.lean

@@ -177,6 +177,7 @@ import Mathlib.Algebra.GCDMonoid.Div
 import Mathlib.Algebra.GCDMonoid.Finset
 import Mathlib.Algebra.GCDMonoid.IntegrallyClosed
 import Mathlib.Algebra.GCDMonoid.Multiset
+import Mathlib.Algebra.GCDMonoid.Nat
 import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.GradedMonoid
 import Mathlib.Algebra.GradedMulAction

Mathlib/Algebra/CharP/CharAndCard.lean

@@ -5,6 +5,7 @@ Authors: Michael Stoll
 -/
 import Mathlib.Algebra.CharP.Basic
 import Mathlib.GroupTheory.Perm.Cycle.Type
+import Mathlib.RingTheory.Coprime.Lemmas
 
 #align_import algebra.char_p.char_and_card from "leanprover-community/mathlib"@"2fae5fd7f90711febdadf19c44dc60fae8834d1b"
 

Mathlib/Algebra/GCDMonoid/Div.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.GCDMonoid.Finset
 import Mathlib.Algebra.GCDMonoid.Basic
 import Mathlib.RingTheory.Int.Basic
 import Mathlib.RingTheory.Polynomial.Content
+import Mathlib.Algebra.GCDMonoid.Nat
 
 #align_import algebra.gcd_monoid.div from "leanprover-community/mathlib"@"b537794f8409bc9598febb79cd510b1df5f4539d"
 

Mathlib/Algebra/GCDMonoid/Nat.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Jens Wagemaker, Aaron Anderson
+-/
+import Mathlib.Algebra.GCDMonoid.Basic
+import Mathlib.Algebra.Ring.Nat
+import Mathlib.Data.Nat.Units
+
+/-!
+# ℕ is a normalized GCD monoid.
+-/
+
+/-- `ℕ` is a gcd_monoid. -/
+instance : GCDMonoid ℕ where
+  gcd := Nat.gcd
+  lcm := Nat.lcm
+  gcd_dvd_left := Nat.gcd_dvd_left
+  gcd_dvd_right := Nat.gcd_dvd_right
+  dvd_gcd := Nat.dvd_gcd
+  gcd_mul_lcm a b := by rw [Nat.gcd_mul_lcm]; rfl
+  lcm_zero_left := Nat.lcm_zero_left
+  lcm_zero_right := Nat.lcm_zero_right
+
+theorem gcd_eq_nat_gcd (m n : ℕ) : gcd m n = Nat.gcd m n :=
+  rfl
+#align gcd_eq_nat_gcd gcd_eq_nat_gcd
+
+theorem lcm_eq_nat_lcm (m n : ℕ) : lcm m n = Nat.lcm m n :=
+  rfl
+#align lcm_eq_nat_lcm lcm_eq_nat_lcm
+
+instance : NormalizedGCDMonoid ℕ :=
+  { (inferInstance : GCDMonoid ℕ),
+    (inferInstance : NormalizationMonoid ℕ) with
+    normalize_gcd := fun _ _ => normalize_eq _
+    normalize_lcm := fun _ _ => normalize_eq _ }

Mathlib/GroupTheory/Exponent.lean

@@ -7,6 +7,7 @@ import Mathlib.Data.ZMod.Quotient
 import Mathlib.GroupTheory.NoncommPiCoprod
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.Algebra.GCDMonoid.Finset
+import Mathlib.Algebra.GCDMonoid.Nat
 import Mathlib.Data.Nat.Factorization.Basic
 import Mathlib.Tactic.ByContra
 import Mathlib.Tactic.Peel

Mathlib/GroupTheory/Perm/Cycle/Type.lean

@@ -8,7 +8,7 @@ import Mathlib.Combinatorics.Enumerative.Partition
 import Mathlib.Data.List.Rotate
 import Mathlib.GroupTheory.Perm.Cycle.Factors
 import Mathlib.GroupTheory.Perm.Closure
-import Mathlib.RingTheory.Int.Basic
+import Mathlib.Algebra.GCDMonoid.Nat
 import Mathlib.Tactic.NormNum.GCD
 
 #align_import group_theory.perm.cycle.type from "leanprover-community/mathlib"@"47adfab39a11a072db552f47594bf8ed2cf8a722"

Mathlib/GroupTheory/Perm/Fin.lean

@@ -313,3 +313,5 @@ theorem isThreeCycle_cycleRange_two {n : ℕ} : IsThreeCycle (cycleRange 2 : Per
 end Fin
 
 end CycleRange
+
+assert_not_exists LinearMap

Mathlib/RingTheory/Int/Basic.lean

@@ -54,31 +54,6 @@ instance : UniqueFactorizationMonoid ℕ :=
 
 end Nat
 
-/-- `ℕ` is a gcd_monoid. -/
-instance : GCDMonoid ℕ where
-  gcd := Nat.gcd
-  lcm := Nat.lcm
-  gcd_dvd_left := Nat.gcd_dvd_left
-  gcd_dvd_right := Nat.gcd_dvd_right
-  dvd_gcd := Nat.dvd_gcd
-  gcd_mul_lcm a b := by rw [Nat.gcd_mul_lcm]; rfl
-  lcm_zero_left := Nat.lcm_zero_left
-  lcm_zero_right := Nat.lcm_zero_right
-
-instance : NormalizedGCDMonoid ℕ :=
-  { (inferInstance : GCDMonoid ℕ),
-    (inferInstance : NormalizationMonoid ℕ) with
-    normalize_gcd := fun _ _ => normalize_eq _
-    normalize_lcm := fun _ _ => normalize_eq _ }
-
-theorem gcd_eq_nat_gcd (m n : ℕ) : gcd m n = Nat.gcd m n :=
-  rfl
-#align gcd_eq_nat_gcd gcd_eq_nat_gcd
-
-theorem lcm_eq_nat_lcm (m n : ℕ) : lcm m n = Nat.lcm m n :=
-  rfl
-#align lcm_eq_nat_lcm lcm_eq_nat_lcm
-
 namespace Int
 
 section NormalizationMonoid