subst_X

Mathlib.RingTheory.MvPowerSeries.Substitution

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

English

For any f, map(algebraMap R S) f equals subst X f.

Русский

Для любого f: map(algebraMap R S) f = subst X f.

LaTeX

$$$\\operatorname{map}(\\operatorname{algebraMap} R S)\\ f = \\operatorname{subst}(\\mathrm{X})\\ f$$$

Lean4

@[simp]
theorem subst_X (ha : HasSubst a) (s : σ) : subst (R := R) a (X s) = a s := by rw [← coe_substAlgHom ha, substAlgHom_X]

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

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

Разделы

Аффилиация

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