trailingDegree_eq_iff_natTrailingDegree_eq

English

For any polynomial p and natural n, if p ≠ 0 then trailingDegree(p) = n.cast iff natTrailingDegree(p) = n.

Русский

Для любого полинома p и натурального n, если p ≠ 0, то хвостовая степень p равна n, эквивалентно natTrailingDegree(p) = n.

LaTeX

$$$p \ne 0 \Rightarrow (\,p.trailin gDegree = n \;\iff\; \operatorname{natTrailingDegree}(p) = n)$$$

Lean4

theorem trailingDegree_eq_iff_natTrailingDegree_eq {p : R[X]} {n : ℕ} (hp : p ≠ 0) :
    p.trailingDegree = n ↔ p.natTrailingDegree = n := by rw [trailingDegree_eq_natTrailingDegree hp, Nat.cast_inj]

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