isPrimitive_primPart — Mathlib

English

The primitive part of any polynomial is primitive.

Русский

Примитивная часть любого многочлена сама примитивна.

LaTeX

$$$p.primPart.IsPrimitive$$$

Lean4

theorem isPrimitive_primPart (p : R[X]) : p.primPart.IsPrimitive :=
  by
  by_cases h : p = 0; · simp [h]
  rw [← content_eq_zero_iff] at h
  rw [isPrimitive_iff_content_eq_one]
  apply mul_left_cancel₀ h
  conv_rhs => rw [p.eq_C_content_mul_primPart, mul_one, content_C_mul, normalize_content]

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