single_zero_mul_eq_smul

Mathlib.RingTheory.HahnSeries.Multiplication

URI: https://scilib.ai/kg/mathlib#HahnSeries.single_zero_mul_eq_smul

← MathLib Explorer

English

Multiplication by a degree-zero term acts as scalar multiplication.

Русский

Умножение на член в степени нуль действует как скалярное умножение.

LaTeX

$$$ (\mathrm{single}\; 0\; r) \cdot x = r \cdot x $$$

Lean4

@[simp]
theorem single_zero_mul_eq_smul [Semiring R] {r : R} {x : HahnSeries Γ R} : single 0 r * x = r • x :=
  by
  ext
  exact coeff_single_zero_mul

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

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

Разделы

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

Аффилиация

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