commute_X

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

The element X_s commutes with every multivariate formal power series φ.

Русский

Элемент X_s коммутирует с любым многообразным формальным степенным рядом φ.

LaTeX

$$$\text{Commute}(\phi, X_s)\quad\text{for all }\phi$$$

Lean4

theorem commute_X (φ : MvPowerSeries σ R) (s : σ) : Commute φ (X s) :=
  φ.commute_monomial.mpr fun _m => Commute.one_right _

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

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

Разделы

Аффилиация

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