Product_of_Coprime_Factors
Provedcoprime-integersproofwiki
If a and b are coprime and both divide c, then a*b divides c.
Preamble
import Mathlib.RingTheory.Int.Basic
Formal statement
theorem Product_of_Coprime_Factors (a b c : ℤ) (hab : IsCoprime a b) (ha : a ∣ c) (hb : b ∣ c) : a * b ∣ c := by sorry
Source