degree_radical_le — Mathlib

English

Over a field k, for a nonzero polynomial a ∈ k[X], the degree of its radical is at most the degree of a.

Русский

Над полем k для не нулевого многочлена a ∈ k[X] порядок радикала не превосходит порядка a.

LaTeX

$$$\\forall a \\in k[X],\\ a \\neq 0 \\Rightarrow \\deg(\\operatorname{radical}(a)) \\le \\deg(a)$$$

Lean4

theorem degree_radical_le {a : k[X]} (h : a ≠ 0) : (radical a).degree ≤ a.degree :=
  degree_le_of_dvd radical_dvd_self h

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