nextCoeffUp_of_constantCoeff_eq_zero

English

If coeff p 0 = 0, then nextCoeffUp p = coeff p (natTrailingDegree(p) + 1).

Русский

Если coeff p 0 = 0, то nextCoeffUp p = coeff p (natTrailingDegree(p) + 1).

LaTeX

$$$ (coeff\ p\ 0 = 0) \Rightarrow nextCoeffUp(p) = coeff(p, natTrailingDegree(p) + 1) $$$

Lean4

theorem nextCoeffUp_of_constantCoeff_eq_zero (p : R[X]) (hp : coeff p 0 = 0) :
    nextCoeffUp p = p.coeff (p.natTrailingDegree + 1) :=
  by
  obtain rfl | hp₀ := eq_or_ne p 0
  · simp
  · rw [nextCoeffUp, if_neg (natTrailingDegree_ne_zero.2 ⟨hp₀, hp⟩)]

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