order_X_pow — Mathlib

English

Let R be a nontrivial semiring. For every natural number n, the order of the formal power series X^n is n.

Русский

Пусть R — ненулевое полукольцо. Для каждого натурального числа n порядок формального степенного ряда X^n равен n.

LaTeX

$$$ \\operatorname{order}(X^{n}) = n $$$

Lean4

/-- The order of the formal power series `X^n` is `n`. -/
@[simp]
theorem order_X_pow (n : ℕ) : order ((X : R⟦X⟧) ^ n) = n :=
  by
  rw [X_pow_eq, order_monomial_of_ne_zero]
  exact one_ne_zero

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