le_order_pow — Mathlib

English

For a formal power series φ and natural n, n times the order of φ is not greater than the order of φ^n.

Русский

Для формального степенного ряда φ и натурального n выполняется n·order(φ) ≤ order(φ^n).

LaTeX

$$$\forall \phi \in R\lbrack\!\!X\rbrack,\ n \in \mathbb{N},\ n\cdot \operatorname{order}(\phi) \le \operatorname{order}(\phi^n)$$$

Lean4

theorem le_order_pow (φ : R⟦X⟧) (n : ℕ) : n • order φ ≤ order (φ ^ n) := by
  induction n with
  | zero => simp
  | succ n hn =>
    simp only [add_smul, one_smul, pow_succ]
    apply le_trans _ (le_order_mul _ _)
    exact add_le_add_right hn φ.order

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