truncLT_smul

Mathlib.RingTheory.HahnSeries.Addition

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

English

The truncation map commutes with scalar multiplication: truncLT c (r•x) = r•truncLT c x.

Русский

Сокращение truncLT с умножением на скаляр commuting: truncLT c (r•x) = r•truncLT c x.

LaTeX

$$$$ \mathrm{truncLT}_c(r\cdot x) = r\cdot \mathrm{truncLT}_c(x). $$$$

Lean4

theorem truncLT_smul [DecidableLT Γ] (c : Γ) (r : R) (x : HahnSeries Γ V) : truncLT c (r • x) = r • truncLT c x := by
  ext; simp

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

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

Разделы

Аффилиация

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