feat(Algebra/Associated): add Associated.map (#10895)

Mathlib/Algebra/Associated.lean

@@ -420,6 +420,11 @@ protected def setoid (α : Type*) [Monoid α] :
   iseqv := ⟨Associated.refl, Associated.symm, Associated.trans⟩
 #align associated.setoid Associated.setoid
 
+theorem map {M N : Type*} [Monoid M] [Monoid N] {F : Type*} [FunLike F M N] [MonoidHomClass F M N]
+    (f : F) {x y : M} (ha : Associated x y) : Associated (f x) (f y) := by
+  obtain ⟨u, ha⟩ := ha
+  exact ⟨Units.map f u, by rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]⟩
+
 end Associated
 
 attribute [local instance] Associated.setoid