gcd_content_eq_of_dvd_sub — Mathlib

English

If C(a) divides p - q, then gcd(a, p.content) = gcd(a, q.content).

Русский

Если C(a) делит p - q, то gcd(a, content(p)) = gcd(a, content(q)).

LaTeX

$$$\gcd(a, p.content) = \gcd(a, q.content)$$$

Lean4

theorem gcd_content_eq_of_dvd_sub {a : R} {p q : R[X]} (h : C a ∣ p - q) :
    GCDMonoid.gcd a p.content = GCDMonoid.gcd a q.content :=
  by
  rw [content_eq_gcd_range_of_lt p (max p.natDegree q.natDegree).succ
      (lt_of_le_of_lt (le_max_left _ _) (Nat.lt_succ_self _))]
  rw [content_eq_gcd_range_of_lt q (max p.natDegree q.natDegree).succ
      (lt_of_le_of_lt (le_max_right _ _) (Nat.lt_succ_self _))]
  apply Finset.gcd_eq_of_dvd_sub
  intro x _
  obtain ⟨w, hw⟩ := h
  use w.coeff x
  rw [← coeff_sub, hw, coeff_C_mul]

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