subst_pow — Mathlib

English

Substitution commutes with powering: substituting into f^n equals (subst a f)^n.

Русский

Подстановка коммутирует с возведением в степень: подстановка в f^n равна (подстановка f)^n.

LaTeX

$$$\forall ha\, (f : PowerSeries R), (n : \mathbb{N}),\ subst a (f^n) = (subst a f)^n$$$

Lean4

theorem subst_pow (ha : HasSubst a) (f : PowerSeries R) (n : ℕ) : subst a (f ^ n) = (subst a f) ^ n := by
  rw [← coe_substAlgHom ha, map_pow]

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