X_pow_mul

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

X_s^n and φ commute: X_s^n · φ = φ · X_s^n.

Русский

X_s^n и φ commute: X_s^n · φ = φ · X_s^n.

LaTeX

$$$X_s^n \cdot \phi = \phi \cdot X_s^n$$$

Lean4

theorem X_pow_mul {φ : MvPowerSeries σ R} {s : σ} {n : ℕ} : X s ^ n * φ = φ * X s ^ n :=
  φ.commute_X_pow s n |>.symm.eq

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

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

Разделы

Аффилиация

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