coeff_nsmul

Mathlib.RingTheory.HahnSeries.Addition

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

English

Coefficient extraction commutes with natural scalar multiplication.

Русский

Извлечение коэффициента коммутирует с умножением на натуральное число.

LaTeX

$$$$ (n\cdot x).coeff = n\cdot x.coeff. $$$$

Lean4

theorem coeff_nsmul {x : HahnSeries Γ R} {n : ℕ} : (n • x).coeff = n • x.coeff :=
  coeff_smul' _ _

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

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

Разделы

Аффилиация

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