dvd_mul_sub_mul_mul_gcd_of_dvd — Mathlib

English

In a ring with gcd structure and domain properties, if p divides a x + b y and p divides c x + d y, then p divides (a d − b c) gcd(x,y).

Русский

В кольце с gcd-структурой и свойством домена: если p делит a x + b y и p делит c x + d y, то p делит (a d − b c) gcd(x,y).

LaTeX

$$p ∣ a x + b y ∧ p ∣ c x + d y ⇒ p ∣ (a d - b c) gcd(x,y)$$

Lean4

theorem dvd_mul_sub_mul_mul_gcd_of_dvd {p a b c d x y : R} [IsDomain R] [GCDMonoid R] (h1 : p ∣ a * x + b * y)
    (h2 : p ∣ c * x + d * y) : p ∣ (a * d - b * c) * gcd x y :=
  by
  rw [← (gcd_mul_left' (a * d - b * c) x y).dvd_iff_dvd_right]
  exact (dvd_gcd_iff _ _ _).2 ⟨dvd_mul_sub_mul_mul_left_of_dvd h1 h2, dvd_mul_sub_mul_mul_right_of_dvd h1 h2⟩

Похожие утверждения