natDegree_radical_le — Mathlib

English

Let a be a polynomial in k[x] over a field k. The radical of a has natural degree not exceeding the natural degree of a; in symbols, natDegree(radical(a)) ≤ natDegree(a).

Русский

Пусть a — многочлен над полем k. Радикал(a) имеет натуральную степень, не превосходящую степень(a); то есть natDegree(radical(a)) ≤ natDegree(a).

LaTeX

$$$\\operatorname{natDegree}(\\operatorname{radical}(a)) \\le \\operatorname{natDegree}(a)$$$

Lean4

theorem natDegree_radical_le {a : k[X]} : (radical a).natDegree ≤ a.natDegree :=
  by
  by_cases ha : a = 0
  · simp [ha]
  · exact natDegree_le_of_dvd radical_dvd_self ha

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