c_eq_algebraMap

Mathlib.RingTheory.MvPowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.c_eq_algebraMap

English

The canonical embedding C of R into MvPowerSeries σ R coincides with the algebraMap from R to MvPowerSeries σ R.

Русский

Каноническое отображение C равно algebraMap: R → MvPowerSeries σ R.

LaTeX

$$$\\mathsf{C} = \\mathrm{algebraMap} R (\\mathrm{MvPowerSeries} \\; \\sigma \\; R)$$$

Lean4

theorem c_eq_algebraMap : C = algebraMap R (MvPowerSeries σ R) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru