substAlgHom_X

Mathlib.RingTheory.PowerSeries.Substitution

URI: https://scilib.ai/kg/mathlib#PowerSeries.substAlgHom_X

English

For a substitution ha, substituting the indeterminate X yields the underlying mv-power-series a.

Русский

Для подстановки ha подстановка X возвращает исходную mv-ряд a.

LaTeX

$$$\\operatorname{substAlgHom}(ha)(X) = a$$$

Lean4

theorem substAlgHom_X (ha : HasSubst a) : substAlgHom ha (X : R⟦X⟧) = a := by
  rw [← Polynomial.coe_X, substAlgHom_coe, Polynomial.aeval_X]

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

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

Разделы

Аффилиация

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