content_eq_gcd_leadingCoeff_content_eraseLead

English

The content of a polynomial p is the gcd of its leading coefficient and the content of eraseLead(p).

Русский

Содержимое полинома p равно НОД ведущего коэффициента и содержимого eraseLead(p).

LaTeX

$$$$ p.content = \\operatorname{GCDMonoid.gcd}(p.leadingCoeff, (eraseLead(p)).content) $$$$

Lean4

theorem content_eq_gcd_leadingCoeff_content_eraseLead (p : R[X]) :
    p.content = GCDMonoid.gcd p.leadingCoeff (eraseLead p).content :=
  by
  by_cases h : p = 0
  · simp [h]
  rw [← leadingCoeff_eq_zero, leadingCoeff, ← Ne, ← mem_support_iff] at h
  rw [content, ← Finset.insert_erase h, Finset.gcd_insert, leadingCoeff, content, eraseLead_support]
  refine congr rfl (Finset.gcd_congr rfl fun i hi => ?_)
  rw [Finset.mem_erase] at hi
  rw [eraseLead_coeff, if_neg hi.1]

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