order_pow — Mathlib

English

For a Hahn series x and a natural number n, the order of the nth power is n times the order of x: ord(x^n) = n·ord(x).

Русский

Для Ханнового ряда x и натурального числа n порядок x^n равен n раз порядка x: ord(x^n) = n·ord(x).

LaTeX

$$$\\operatorname{ord}(x^n) = n \\cdot \\operatorname{ord}(x), \\quad n \\in \\mathbb{N}.$$$

Lean4

@[simp]
theorem order_pow {Γ} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] [NoZeroDivisors R]
    (x : HahnSeries Γ R) (n : ℕ) : (x ^ n).order = n • x.order := by
  induction n with
  | zero => simp
  | succ h IH =>
    rcases eq_or_ne x 0 with (rfl | hx); · simp
    rw [pow_succ, order_mul (pow_ne_zero _ hx) hx, succ_nsmul, IH]

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