natDegree_primPart — Mathlib

English

The nat-degree of the primitive part equals the nat-degree of the polynomial.

Русский

Порядковая степень примPart равна порядковой степени оригинального многочлена.

LaTeX

$$$p.primPart.natDegree = p.natDegree$$$

Lean4

theorem natDegree_primPart (p : R[X]) : p.primPart.natDegree = p.natDegree :=
  by
  by_cases h : C p.content = 0
  · rw [C_eq_zero, content_eq_zero_iff] at h
    simp [h]
  conv_rhs => rw [p.eq_C_content_mul_primPart, natDegree_mul h p.primPart_ne_zero, natDegree_C, zero_add]

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