C_inv

Mathlib.RingTheory.PowerSeries.Inverse

URI: https://scilib.ai/kg/mathlib#PowerSeries.C_inv

English

For any r ∈ k, the constant power series C(r) is invertible with inverse C(r)^{-1} = C(r^{-1}).

Русский

Для любого r ∈ k константный степенной ряд C(r) обратим, обратный к нему равен C(r^{-1}).

LaTeX

$$$ (C\,r)^{-1} = C\,r^{-1}. $$$

Lean4

@[simp]
theorem C_inv (r : k) : (C r)⁻¹ = C r⁻¹ :=
  MvPowerSeries.C_inv _

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

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

Разделы

Аффилиация

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