Divisor_of_Sum_of_Coprime_Integers
Provedcoprime-integersdivisorsnumber-theoryproofwiki
If a and b are coprime and c divides a + b, then a is coprime to c and b is coprime to c.
Preamble
import Mathlib.RingTheory.Int.Basic
Formal statement
theorem Divisor_of_Sum_of_Coprime_Integers (a b c : ℤ) (hab : IsCoprime a b) (hc : c ∣ (a + b)) : IsCoprime a c ∧ IsCoprime b c := by sorry
Source