Common_Divisor_in_Integral_Domain_Divides_Linear_Combination
Proveddivisibilityproofwiki
In an integral domain, if c divides both a and b, then c divides pa + qb for all p, q.
Preamble
import Mathlib.RingTheory.Int.Basic
Formal statement
theorem Common_Divisor_in_Integral_Domain_Divides_Linear_Combination {D : Type _} [CommRing D] [IsDomain D] {a b c : D} (ha : c ∣ a) (hb : c ∣ b) (p q : D) : c ∣ (p * a + q * b) := by sorrySource