leadingCoeff_mul_prod_normalizedFactors

English

For any polynomial a over a field, a equals the product of its leading coefficient embedded as a constant and the product of its normalized factors.

Русский

Для любого многочлена a над полем, a равно произведению его ведущего коэффициента, инкапсулированного как константа, на произведение его нормализованных множителей.

LaTeX

$$$C\,a.leadingCoeff \cdot \bigl(normalizedFactors\ a\bigr).prod = a$.$$

Lean4

/-- The normalized factors of a polynomial over a field times its leading coefficient give
the polynomial.
-/
theorem leadingCoeff_mul_prod_normalizedFactors [DecidableEq R] (a : R[X]) :
    C a.leadingCoeff * (normalizedFactors a).prod = a :=
  by
  by_cases ha : a = 0
  · simp [ha]
  rw [prod_normalizedFactors_eq, normalize_apply, coe_normUnit, CommGroupWithZero.coe_normUnit, mul_comm, mul_assoc, ←
      map_mul, inv_mul_cancel₀] <;>
    simp_all

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