feat: Nat.lcm_mul_left and Nat.lcm_mul_right (#6990)

Add two lemmas about `Nat.lcm`. These results mirror [Nat.gcd_mul_left](https://leanprover-community.github.io/mathlib4_docs/Std/Data/Nat/Gcd.html#Nat.gcd_mul_left) present in Std.



Co-authored-by: Arend Mellendijk <FLDutchmann@users.noreply.github.com>

Mathlib/Data/Int/GCD.lean

@@ -499,6 +499,12 @@ theorem lcm_dvd {i j k : ℤ} : i ∣ k → j ∣ k → (lcm i j : ℤ) ∣ k :=
   exact coe_nat_dvd_left.mpr (Nat.lcm_dvd (natAbs_dvd_natAbs.mpr hi) (natAbs_dvd_natAbs.mpr hj))
 #align int.lcm_dvd Int.lcm_dvd
 
+theorem lcm_mul_left {m n k : ℤ} : (m * n).lcm (m * k) = natAbs m * n.lcm k := by
+  simp_rw [Int.lcm, natAbs_mul, Nat.lcm_mul_left]
+
+theorem lcm_mul_right {m n k : ℤ} : (m * n).lcm (k * n) = m.lcm k * natAbs n := by
+  simp_rw [Int.lcm, natAbs_mul, Nat.lcm_mul_right]
+
 end Int
 
 @[to_additive gcd_nsmul_eq_zero]

Mathlib/Data/Nat/GCD/Basic.lean

@@ -128,6 +128,15 @@ theorem lcm_pos {m n : ℕ} : 0 < m → 0 < n → 0 < m.lcm n := by
   exact lcm_ne_zero
 #align nat.lcm_pos Nat.lcm_pos
 
+theorem lcm_mul_left {m n k : ℕ} : (m * n).lcm (m * k) = m * n.lcm k := by
+  apply dvd_antisymm
+  · exact lcm_dvd (mul_dvd_mul_left m (dvd_lcm_left n k)) (mul_dvd_mul_left m (dvd_lcm_right n k))
+  · have h : m ∣ lcm (m * n) (m * k) := (dvd_mul_right m n).trans (dvd_lcm_left (m * n) (m * k))
+    rw [←dvd_div_iff h, lcm_dvd_iff, dvd_div_iff h, dvd_div_iff h, ←lcm_dvd_iff]
+
+theorem lcm_mul_right {m n k : ℕ} : (m * n).lcm (k * n) = m.lcm k * n := by
+ rw [mul_comm, mul_comm k n, lcm_mul_left, mul_comm]
+
 /-!
 ### `Coprime`