inv

Mathlib.RingTheory.PowerSeries.Inverse

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

English

Over a field k, the inverse operation on k⟦X⟧ is defined as MvPowerSeries.inv.

Русский

Далее над полем k операция обратного на k⟦X⟧ задаётся как MvPowerSeries.inv.

LaTeX

$$$ inv_{k}(\cdot) = \mathrm{MvPowerSeries.inv}(\cdot) $$$

Lean4

/-- The inverse 1/f of a power series f defined over a field -/
protected def inv : k⟦X⟧ → k⟦X⟧ :=
  MvPowerSeries.inv

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

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

Разделы

Аффилиация

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