natDegree_mul_leadingCoeff_self_inv

English

For p ∈ K[X], natDegree(p · (leadingCoeff p)^{-1}) = natDegree p.

Русский

Для многочлена p над K: natDegree(p · (leadingCoeff p)^{-1}) = natDegree p.

LaTeX

$$$\\operatorname{natDegree}\\bigl(p \\cdot C(\\operatorname{leadingCoeff}(p))^{-1}\\bigr) = \\operatorname{natDegree}(p)$$$

Lean4

theorem natDegree_mul_leadingCoeff_self_inv (p : K[X]) : natDegree (p * C (leadingCoeff p)⁻¹) = natDegree p :=
  natDegree_eq_of_degree_eq
    (degree_mul_leadingCoeff_self_inv _)
      -- `simp` normal form of `degree_mul_leadingCoeff_self_inv`

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