aeval

Mathlib.RingTheory.PowerSeries.Evaluation

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

← MathLib Explorer

English

If a = a' then aeval a equals aeval a' (under HasEval a).

Русский

Если a = a', то aeval a = aeval a' (при HasEval a).

LaTeX

$$$a = a' \Rightarrow aeval a = aeval a'$$$

Lean4

/-- For `HasEval a`,
the evaluation homomorphism at `a` on `PowerSeries`, as an `AlgHom`. -/
noncomputable def aeval (ha : HasEval a) : PowerSeries R →ₐ[R] S :=
  MvPowerSeries.aeval (hasEval ha)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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