content_eq_gcd_range_of_lt — Mathlib

English

For p ∈ R[X], n ∈ ℕ, if natDegree p < n, then p.content equals gcd of p.coeff over Finset.range n.

Русский

Для p ∈ R[X], n ∈ ℕ, если natDegree p < n, то p.content является НОД коэффициентов p по Finset.range n.

LaTeX

$$$$ p.content = (\\operatorname{Finset}.range(n)).gcd(p.coeff) \\quad \\text{if } p.natDegree < n $$$$

Lean4

theorem content_eq_gcd_range_of_lt (p : R[X]) (n : ℕ) (h : p.natDegree < n) :
    p.content = (Finset.range n).gcd p.coeff :=
  by
  apply dvd_antisymm_of_normalize_eq normalize_content Finset.normalize_gcd
  · rw [Finset.dvd_gcd_iff]
    intro i _
    apply content_dvd_coeff _
  · apply Finset.gcd_mono
    intro i
    simp only [mem_support_iff, Ne, Finset.mem_range]
    contrapose!
    intro h1
    apply coeff_eq_zero_of_natDegree_lt (lt_of_lt_of_le h h1)

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