trailingDegree_eq_natTrailingDegree

English

If p is nonzero, then trailingDegree(p) equals natTrailingDegree(p) viewed as an extended natural.

Русский

Если p не нуль, то хвостовая степень p равна natTrailingDegree(p), приведённой к ∞-множителю.

LaTeX

$$$p \ne 0 \Rightarrow \operatorname{trailingDegree}(p) = (\operatorname{natTrailingDegree}(p) : \mathbb{N}_\infty)$$$

Lean4

theorem trailingDegree_eq_natTrailingDegree (hp : p ≠ 0) : trailingDegree p = (natTrailingDegree p : ℕ∞) :=
  .symm <| ENat.coe_toNat <| mt trailingDegree_eq_top.1 hp

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