coe_pow — Mathlib

English

Taking powers commutes with the embedding: the power series obtained by raising a Laurent series f to the nth power matches the nth power of the embedded power series of f.

Русский

Возведение в степень и вложение в степенной ряд взаимно согласованы: степенной ряд, полученный из лорентова ряда f при возведении в n-ю степень, совпадает с n-й степенной степенью вложенного ряда f.

LaTeX

$$$\forall n\in\mathbb{N},\; ((f^n) : R\langle X\rangle) = (ofPowerSeries\,\mathbb{Z}\,R\,f)^n.$$$

Lean4

@[norm_cast]
theorem coe_pow (n : ℕ) : ((f ^ n : R⟦X⟧) : R⸨X⸩) = (ofPowerSeries ℤ R f) ^ n :=
  (ofPowerSeries ℤ R).map_pow _ _

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