order_X — Mathlib

English

Let R be a nontrivial semiring. In the ring of formal power series R[[X]], the order of the indeterminate X is 1.

Русский

Пусть R — ненулевое полукольцо. В кольце формальных степенных рядов R[[X]] порядок переменной X равен 1.

LaTeX

$$$ \\operatorname{order}(X) = 1 $$$

Lean4

/-- The order of the formal power series `X` is `1`. -/
@[simp]
theorem order_X : order (X : R⟦X⟧) = 1 := by
  simpa only [Nat.cast_one] using order_monomial_of_ne_zero 1 (1 : R) one_ne_zero

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