degree_mul_leadingCoeff_inv — Mathlib

English

For any p, q with q ≠ 0, the degree of p · (leadingCoeff q)^{-1} equals the degree of p.

Русский

Для любых p и q с q ≠ 0, deg(p · (leadingCoeff q)^{-1}) = deg(p).

LaTeX

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

Lean4

theorem degree_mul_leadingCoeff_inv (p : K[X]) {q : K[X]} (h : q ≠ 0) : degree (p * C (leadingCoeff q)⁻¹) = degree p :=
  by
  have h₁ : (leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)
  rw [degree_mul_C h₁]

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