algebraMap_apply — Mathlib

English

For r ∈ R, algebraMap R (MvPowerSeries σ A) r equals C (algebraMap R A r).

Русский

Для r ∈ R отображение algebraMap R (MvPowerSeries σ A) r равно C (algebraMap R A r).

LaTeX

$$$\\mathrm{algebraMap}_R^{\\mathrm{MvPowerSeries}}(r) = C\\big(\\mathrm{algebraMap}_R^A(r)\\big)$$$

Lean4

theorem algebraMap_apply {r : R} : algebraMap R (MvPowerSeries σ A) r = C (algebraMap R A r) :=
  by
  change (MvPowerSeries.map (algebraMap R A)).comp C r = _
  simp

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