Quick question (Euclid's Lemma)

Stream: new members

[Nathan]

Is there a version of Nat.Coprime.dvd_of_dvd_mul_left for Ints?

example (a b c : ℕ) (h : a ∣ b * c) (hc : Nat.Coprime a b) : a ∣ c :=
  Nat.Coprime.dvd_of_dvd_mul_left hc h

[Ruben Van de Velde]

import Mathlib
example (a b c : ℤ) (h : a ∣ b * c) (hc : IsCoprime a b) : a ∣ c := by apply?

[Ruben Van de Velde]

Or you can guess the name

[Nathan]

thanks :pray: