feat: port Algebra.GCDMonoid.Basic (#1135)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

Author: 3 people

Mathlib.lean

@@ -12,6 +12,7 @@ import Mathlib.Algebra.Field.Basic
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Field.Opposite
 import Mathlib.Algebra.Field.Power
+import Mathlib.Algebra.GCDMonoid.Basic
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Commutator
 import Mathlib.Algebra.Group.Commute

Mathlib/Algebra/Associated.lean

@@ -838,7 +838,7 @@ instance : Preorder (Associates α) where
   le_refl := dvd_refl
   le_trans a b c := dvd_trans
 
-/-- `associates.mk` as a `monoid_hom`. -/
+/-- `Associates.mk` as a `MonoidHom`. -/
 protected def mkMonoidHom : α →* Associates α :=
   {
     toFun := Associates.mk
@@ -847,9 +847,9 @@ protected def mkMonoidHom : α →* Associates α :=
 #align associates.mk_monoid_hom Associates.mkMonoidHom
 
 @[simp]
-theorem mk_monoid_hom_apply (a : α) : Associates.mkMonoidHom a = Associates.mk a :=
+theorem mk_monoidHom_apply (a : α) : Associates.mkMonoidHom a = Associates.mk a :=
   rfl
-#align associates.mk_monoid_hom_apply Associates.mk_monoid_hom_apply
+#align associates.mk_monoid_hom_apply Associates.mk_monoidHom_apply
 
 theorem associated_map_mk {f : Associates α →* α} (hinv : Function.RightInverse f Associates.mk)
     (a : α) : a ~ᵤ f (Associates.mk a) :=

Mathlib/Algebra/Divisibility/Basic.lean

@@ -74,6 +74,9 @@ alias dvd_trans ← Dvd.dvd.trans
 instance : IsTrans α (· ∣ ·) :=
   ⟨fun _ _ _ => dvd_trans⟩
 
+/-- Transitivity of `|` for use in `calc` blocks -/
+instance : @Trans α α α Dvd.dvd Dvd.dvd Dvd.dvd := ⟨dvd_trans⟩
+
 @[simp]
 theorem dvd_mul_right (a b : α) : a ∣ a * b :=
   Dvd.intro b rfl