algebraMap_apply — Mathlib

English

Applying the algebra map to a scalar r from R yields the constant power series with coefficient algebraMap r: algebraMap R A⟦X⟧ r = C (algebraMap R A r).

Русский

Применение алгебраMap к скалярy r из R даёт константный ряд с коэффициентом algebraMap r: algebraMap R A⟦X⟧ r = C (algebraMap R A r).

LaTeX

$$$\\operatorname{algebraMap} R (A\\llbracket X\\rrbracket)\\, r = C\\bigl(\\operatorname{algebraMap} R A\\, r\\bigr)$$$

Lean4

theorem algebraMap_apply {r : R} : algebraMap R A⟦X⟧ r = C (algebraMap R A r) :=
  MvPowerSeries.algebraMap_apply

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