X_inv

Mathlib.RingTheory.MvPowerSeries.Inverse

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

English

For each index s in σ, the inverse of the monomial X_s is the zero series.

Русский

Для каждой переменной X_s ее обратное равно нулевому ряду.

LaTeX

$$$(X_s)^{-1} = 0$$$

Lean4

@[simp]
theorem X_inv (s : σ) : (X s : MvPowerSeries σ k)⁻¹ = 0 := by rw [inv_eq_zero, constantCoeff_X]

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

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

Разделы

Аффилиация

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