content_eq_gcd_range_succ — Mathlib

English

For any p ∈ R[X], p.content equals gcd of p.coeff over Finset.range(p.natDegree.succ).

Русский

Для любого p ∈ R[X] содержимое p равно НОД коэффициентов p по Finset.range(p.natDegree.succ).

LaTeX

$$$$ p.content = (\\operatorname{Finset}.range(p.natDegree.succ)).gcd(p.coeff) $$$$

Lean4

theorem content_eq_gcd_range_succ (p : R[X]) : p.content = (Finset.range p.natDegree.succ).gcd p.coeff :=
  content_eq_gcd_range_of_lt _ _ (Nat.lt_succ_self _)

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