natTrailingDegree_le_of_trailingDegree_le

English

If (n ≤ trailingDegree(p)) then n ≤ natTrailingDegree(p).

Русский

Если (n ≤ trailingDegree(p)), тогда n ≤ natTrailingDegree(p).

LaTeX

$$$(n : \mathbb{N}_\infty) \le \operatorname{trailingDegree}(p) \Rightarrow n \le \operatorname{natTrailingDegree}(p)$$$

Lean4

theorem natTrailingDegree_le_of_trailingDegree_le {n : ℕ} {hp : p ≠ 0} (H : (n : ℕ∞) ≤ trailingDegree p) :
    n ≤ natTrailingDegree p := by rwa [trailingDegree_eq_natTrailingDegree hp, Nat.cast_le] at H

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