single_pow — Mathlib

English

For a in Γ, r in R, the nth power of the Hahn series concentrated at a with coefficient r is the Hahn series concentrated at n·a with coefficient r^n.

Русский

Пусть a ∈ Γ, r ∈ R. Возведение в степень n Hahn-переменной, сосредоточенной в a с коэффициентом r, равно Hahn-переменной, сосредоточенной в n·a с коэффициентом r^n.

LaTeX

$$$ \operatorname{single}(a,r)^n = \operatorname{single}(n \cdot a, r^n) $$$

Lean4

@[simp]
theorem single_pow (a : Γ) (n : ℕ) (r : R) : single a r ^ n = single (n • a) (r ^ n) := by
  induction n with
  | zero => ext; simp only [pow_zero, coeff_one, zero_smul, coeff_single]
  | succ n IH => rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]

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