map_X

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

X s is fixed by any coefficient map: map f (X s) = X s.

Русский

X s остаётся неизменным при отображении по коэффициентам: map f (X s) = X s.

LaTeX

$$$\\mathrm{map}\\ f (X\\ s) = X\\ s$$$

Lean4

@[simp]
theorem map_X (s : σ) : map f (X s) = X s := by simp [MvPowerSeries.X]

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

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

Разделы

Аффилиация

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