content_dvd_coeff — Mathlib

English

An irreducible nonconstant polynomial over a domain is primitive.

Русский

irreducible непостоянный полином над доменом примитивен.

LaTeX

$$$$ \\text{Irreducible}(p) \\land p.natDegree \\ne 0 \\Rightarrow p.IsPrimitive $$$$

Lean4

theorem content_dvd_coeff {p : R[X]} (n : ℕ) : p.content ∣ p.coeff n :=
  by
  by_cases h : n ∈ p.support
  · apply Finset.gcd_dvd h
  rw [mem_support_iff, Classical.not_not] at h
  rw [h]
  apply dvd_zero

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