order_pow — Mathlib

English

For every natural number n, the order of X^n is n.

Русский

Пусть n — натуральное число. Порядок $X^n$ равен $n$.

LaTeX

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

Lean4

theorem order_pow [Nontrivial R] (φ : R⟦X⟧) (n : ℕ) : order (φ ^ n) = n • order φ :=
  by
  rcases subsingleton_or_nontrivial R with hR | hR
  · simp only [Subsingleton.eq_zero φ, order_zero, nsmul_eq_mul]
    by_cases hn : n = 0
    · simp [hn, pow_zero]
    · simp [zero_pow hn, ENat.mul_top', if_neg hn]
  induction n with
  | zero => simp
  | succ n hn => simp only [add_smul, one_smul, pow_succ, order_mul, hn]

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