degree_lt_degree_mul_X — Mathlib

English

If p ≠ 0, then deg(p) < deg(p · X).

Русский

Если p ≠ 0, то deg(p) < deg(p · X).

LaTeX

$$$ p \neq 0 \Rightarrow \deg(p) < \deg(p \cdot X). $$$

Lean4

theorem degree_lt_degree_mul_X (hp : p ≠ 0) : p.degree < (p * X).degree :=
  by
  haveI := Nontrivial.of_polynomial_ne hp
  have : leadingCoeff p * leadingCoeff X ≠ 0 := by simpa
  rw [degree_mul' this, degree_eq_natDegree hp, degree_X, ← Nat.cast_one, ← Nat.cast_add]
  norm_cast
  exact Nat.lt_succ_self _

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