mul_left

Mathlib.RingTheory.MvPowerSeries.Evaluation

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.HasEval.mul_left

← MathLib Explorer

English

Multiplying a HasEval x by a left multiplier c(s) preserves HasEval; i.e., c * x has HasEval.

Русский

Умножение HasEval-значения слева сохраняет HasEval.

LaTeX

$$$HasEval(c * x)$$$

Lean4

theorem mul_left [IsLinearTopology S S] (c : σ → S) {x : σ → S} (hx : HasEval x) : HasEval (c * x)
    where
  hpow s := (hx.hpow s).mul_left (c s)
  tendsto_zero := IsLinearTopology.tendsto_mul_zero_of_right _ _ hx.tendsto_zero

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

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

Разделы

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

Аффилиация

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