X_mul

Mathlib.RingTheory.MvPowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.X_mul

English

Multiplication by X_s commutes with any φ: X_s · φ = φ · X_s.

Русский

Умножение на X_s коммутирует с любым φ: X_s · φ = φ · X_s.

LaTeX

$$$X_s \cdot \phi = \phi \cdot X_s$$$

Lean4

theorem X_mul {φ : MvPowerSeries σ R} {s : σ} : X s * φ = φ * X s :=
  φ.commute_X s |>.symm.eq

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

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

Разделы

Аффилиация

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