Divisors_of_Product_of_Coprime_Integers
Provedcoprime-integersnumber-theoryproofwiki
Let a divide bc where b and c are coprime. Then a = rs where r divides b and s divides c, uniquely up to sign.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Divisors_of_Product_of_Coprime_Integers (a b c : ℤ) (hab : IsCoprime b c) (h : a ∣ b * c) : ∃ r s : ℤ, a = r * s ∧ r ∣ b ∧ s ∣ c := by sorry
Source