natTrailingDegree_eq_of_trailingDegree_eq

English

If trailingDegree(p) = trailingDegree(q) in any semiring S, then natTrailingDegree(p) = natTrailingDegree(q).

Русский

Если для полиномов p и q из S[X] хвостовые степени равны, то natTrailingDegree(p) = natTrailingDegree(q).

LaTeX

$$$\operatorname{trailingDegree}(p) = \operatorname{trailingDegree}(q) \Rightarrow \operatorname{natTrailingDegree}(p) = \operatorname{natTrailingDegree}(q)$$$

Lean4

theorem natTrailingDegree_eq_of_trailingDegree_eq [Semiring S] {q : S[X]} (h : trailingDegree p = trailingDegree q) :
    natTrailingDegree p = natTrailingDegree q :=
  by
  unfold natTrailingDegree
  rw [h]

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