substAlgHom_apply

Mathlib.RingTheory.MvPowerSeries.Substitution

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

English

For HasSubst a, and f, the action of substAlgHom on f equals the direct substitution: substAlgHom ha f = subst a f.

Русский

Для HasSubst a и f выполнено: substAlgHom ha f = subst a f.

LaTeX

$$@[simp] $\\operatorname{substAlgHom ha} f = \\operatorname{subst} a f$$$

Lean4

@[simp]
theorem substAlgHom_apply (ha : HasSubst a) (f : MvPowerSeries σ R) : substAlgHom ha f = subst a f := by
  rw [coe_substAlgHom]

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

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

Разделы

Аффилиация

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