roots_normalize — Mathlib

English

The multiset of roots is preserved by normalization: the roots of normalize p are exactly the roots of p.

Русский

Множество корней сохраняется под нормализацией: корни normalize p совпадают с корнями p.

LaTeX

$$$\text{roots}(\operatorname{normalize}(p)) = \text{roots}(p).$$$

Lean4

theorem roots_normalize {p : R[X]} : (normalize p).roots = p.roots := by
  rw [normalize_apply, mul_comm, coe_normUnit, roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero]

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