degree_mul_leadingCoeff_self_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem degree_mul_leadingCoeff_self_inv (p : K[X]) : degree (p * C (leadingCoeff p)⁻¹) = degree p :=
  by
  by_cases hp : p = 0
  · simp [hp]
  exact degree_mul_leadingCoeff_inv _ hp

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