degree_leadingCoeff_inv — Mathlib

English

For p ≠ 0, the degree of the constant polynomial inverse of the leading coefficient is zero.

Русский

При p ≠ 0 степень константного множителя, обратного ведущему коэффициенту, равна нулю.

LaTeX

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

Lean4

theorem degree_leadingCoeff_inv {p : K[X]} (hp0 : p ≠ 0) : degree (C (leadingCoeff p)⁻¹) = 0 := by simp [hp0]

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