smul_eq_C_mul

Mathlib.RingTheory.PowerSeries.Basic

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

English

For f ∈ R⟦X⟧ and a ∈ R, a • f = C a * f; scalar multiplication corresponds to multiplication by the constant series C a.

Русский

Для f ∈ R⟦X⟧ и a ∈ R, a • f = C a * f; скалярное умножение эквивалентно умножению на константный ряд C a.

LaTeX

$$$a \cdot f = C(a) \cdot f$$$

Lean4

theorem smul_eq_C_mul (f : R⟦X⟧) (a : R) : a • f = C a * f :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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