coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt

English

If trailingDegree p < trailingDegree q, then coeff q (natTrailingDegree p) = 0.

Русский

Если trailingDegree p < trailingDegree q, то coeff q (natTrailingDegree p) = 0.

LaTeX

$$$ trailingDegree(p) < trailingDegree(q) \Rightarrow coeff(q, natTrailingDegree(p)) = 0 $$$

Lean4

theorem coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt (h : trailingDegree p < trailingDegree q) :
    coeff q (natTrailingDegree p) = 0 :=
  coeff_eq_zero_of_lt_trailingDegree <| natTrailingDegree_le_trailingDegree.trans_lt h

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