feat(algebra/gcd_monoid): move the gcd_monoid nat instance (#7180)

moves `gcd_monoid nat` instance, removes corresponding todos.

removes:
* `nat.normalize_eq` -- use `normalize_eq` instead

renames:
* `nat.gcd_eq_gcd` to `gcd_eq_nat_gcd`
* `nat.lcm_eq_lcm` to `lcm_eq_nat_lcm`



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Author: 3 people

src/algebra/gcd_monoid.lean

@@ -2,17 +2,13 @@
 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
-
-TODO: Provide a GCD monoid instance for `ℕ`, port GCD facts about nats
-TODO: Generalize normalization monoids commutative (cancellative) monoids with or without zero
-TODO: Generalize GCD monoid to not require normalization in all cases
 -/
+
 import algebra.associated
 import data.nat.gcd
 import algebra.group_power.lemmas
 
 /-!
-
 # Monoids with normalization functions, `gcd`, and `lcm`
 
 This file defines extra structures on `comm_cancel_monoid_with_zero`s, including `integral_domain`s.
@@ -24,6 +20,8 @@ This file defines extra structures on `comm_cancel_monoid_with_zero`s, including
 * `gcd_monoid_of_exists_gcd`
 * `gcd_monoid_of_exists_lcm`
 
+For the `gcd_monoid` instances on `ℕ` and `Z`, see `ring_theory.int.basic`.
+
 ## Implementation Notes
 
 * `normalization_monoid` is defined by assigning to each element a `norm_unit` such that multiplying
@@ -48,15 +46,13 @@ without zero.
 
 ## TODO
 
-* Provide a GCD monoid instance for `ℕ`, port GCD facts about nats, definition of coprime
+* Port GCD facts about nats, definition of coprime
 * Generalize normalization monoids to commutative (cancellative) monoids with or without zero
 * Generalize GCD monoid to not require normalization in all cases
 
-
 ## Tags
 
 divisibility, gcd, lcm, normalize
-
 -/
 
 variables {α : Type*}
@@ -822,27 +818,4 @@ gcd_monoid_of_lcm
   (λ a b c ac ab, normalize_dvd_iff.2 ((classical.some_spec (h c b) a).1 ⟨ac, ab⟩))
   (λ a b, normalize_idem _)
 
-/-- `ℕ` is a `gcd_monoid` -/
-instance : gcd_monoid ℕ :=
-{ 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,
-  normalize_gcd       := λ a b, nat.mul_one (a.gcd b),
-  gcd_mul_lcm         := λ a b, (a.gcd_mul_lcm b).trans (mul_one (a * b)).symm,
-  lcm_zero_left       := nat.lcm_zero_left,
-  lcm_zero_right      := nat.lcm_zero_right,
-  norm_unit           := λ _, 1,
-  norm_unit_zero      := rfl,
-  norm_unit_mul       := λ _ _ _ _, rfl,
-  norm_unit_coe_units := λ u, eq_inv_of_eq_inv
-    (by rw [one_inv, units.ext_iff, units.coe_one, nat.is_unit_iff.mp u.is_unit]) }
-
-@[simp] lemma nat.normalize_eq (n : ℕ) : normalize n = n := n.mul_one
-
-lemma nat.gcd_eq_gcd (m n : ℕ) : gcd m n = nat.gcd m n := rfl
-
-lemma nat.lcm_eq_lcm (m n : ℕ) : lcm m n = nat.lcm m n := rfl
-
 end constructors

src/group_theory/perm/cycle_type.lean

@@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
 
-import combinatorics.partition
 import algebra.gcd_monoid.multiset
-import tactic.linarith
+import combinatorics.partition
 import group_theory.perm.cycles
 import group_theory.sylow
+import ring_theory.int.basic
+import tactic.linarith
 
 /-!
 # Cycle Types
@@ -154,9 +155,8 @@ cycle_induction_on (λ τ : perm α, sign τ = (τ.cycle_type.map (λ n, -(-1 :
 lemma lcm_cycle_type (σ : perm α) : σ.cycle_type.lcm = order_of σ :=
 cycle_induction_on (λ τ : perm α, τ.cycle_type.lcm = order_of τ) σ
   (by rw [cycle_type_one, lcm_zero, order_of_one])
-  (λ σ hσ, by rw [hσ.cycle_type, ←singleton_coe, lcm_singleton, order_of_is_cycle hσ,
-    nat.normalize_eq])
-  (λ σ τ hστ hc hσ hτ, by rw [hστ.cycle_type, lcm_add, nat.lcm_eq_lcm, hστ.order_of, hσ, hτ])
+  (λ σ hσ, by rw [hσ.cycle_type, ←singleton_coe, lcm_singleton, order_of_is_cycle hσ, normalize_eq])
+  (λ σ τ hστ hc hσ hτ, by rw [hστ.cycle_type, lcm_add, lcm_eq_nat_lcm, hστ.order_of, hσ, hτ])
 
 lemma dvd_of_mem_cycle_type {σ : perm α} {n : ℕ} (h : n ∈ σ.cycle_type) : n ∣ order_of σ :=
 begin
@@ -437,7 +437,7 @@ by rwa [is_three_cycle, cycle_type_inv]
 lemma order_of {g : perm α} (ht : is_three_cycle g) :
   order_of g = 3 :=
 by rw [←lcm_cycle_type, ht.cycle_type, multiset.singleton_eq_singleton,
-  multiset.lcm_singleton, nat.normalize_eq]
+  multiset.lcm_singleton, normalize_eq]
 
 lemma is_three_cycle_sq {g : perm α} (ht : is_three_cycle g) :
   is_three_cycle (g * g) :=

src/ring_theory/int/basic.lean

@@ -85,6 +85,23 @@ instance : unique_factorization_monoid ℕ :=
 
 end nat
 
+/-- `ℕ` is a gcd_monoid. -/
+instance : gcd_monoid ℕ :=
+{ gcd := nat.gcd,
+  lcm := nat.lcm,
+  gcd_dvd_left := nat.gcd_dvd_left ,
+  gcd_dvd_right := nat.gcd_dvd_right,
+  dvd_gcd := λ a b c, nat.dvd_gcd,
+  normalize_gcd := λ a b, normalize_eq _,
+  gcd_mul_lcm := λ a b, by rw [normalize_eq _, nat.gcd_mul_lcm],
+  lcm_zero_left := nat.lcm_zero_left,
+  lcm_zero_right := nat.lcm_zero_right,
+  .. (infer_instance : normalization_monoid ℕ) }
+
+lemma gcd_eq_nat_gcd (m n : ℕ) : gcd m n = nat.gcd m n := rfl
+
+lemma lcm_eq_nat_lcm (m n : ℕ) : lcm m n = nat.lcm m n := rfl
+
 namespace int
 
 section normalization_monoid