coe_pow — Mathlib

English

Embedding commutes with taking powers: (φ^n)ᶠ = (φᶠ)^n.

Русский

Встраивание сохраняет возведение в степень: (φ^n)ᶠ = (φᶠ)^n.

LaTeX

$$$((\\varphi^n : \\mathrm{MvPolynomial}_{\\sigma} R) : \\mathrm{MvPowerSeries}_{\\sigma} R) = (\\varphi : \\mathrm{MvPowerSeries}_{\\sigma} R)^n$$$

Lean4

@[simp, norm_cast]
theorem coe_pow (n : ℕ) : ((φ ^ n : MvPolynomial σ R) : MvPowerSeries σ R) = (φ : MvPowerSeries σ R) ^ n :=
  coeToMvPowerSeries.ringHom.map_pow _ _

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