inv_eq_iff_mul_eq_one

Mathlib.RingTheory.PowerSeries.Inverse

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

English

Let φ, ψ be formal power series with constantCoeff ψ ≠ 0. Then ψ^{-1} = φ if and only if φ ψ = 1.

Русский

Пусть φ, ψ — степенные ряды с c_0(ψ) ≠ 0. Тогда ψ^{-1} = φ ⇔ φ ψ = 1.

LaTeX

$$$ c_0(\psi) \neq 0 \Rightarrow (\psi^{-1} = \phi \iff \phi \psi = 1). $$$

Lean4

theorem inv_eq_iff_mul_eq_one {φ ψ : k⟦X⟧} (h : constantCoeff ψ ≠ 0) : ψ⁻¹ = φ ↔ φ * ψ = 1 :=
  MvPowerSeries.inv_eq_iff_mul_eq_one h

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

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

Разделы

Аффилиация

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