invOfUnit_eq

Mathlib.RingTheory.MvPowerSeries.Inverse

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

English

If constantCoeff φ = u, then invOfUnit φ u = φ⁻¹.

Русский

Если постоянный коэффициент φ равен u, то invOfUnit φ u = φ⁻¹.

LaTeX

$$$ invOfUnit(\varphi, u) = \varphi^{-1} $$$

Lean4

@[simp]
theorem invOfUnit_eq (φ : MvPowerSeries σ k) (h : constantCoeff φ ≠ 0) : invOfUnit φ (Units.mk0 _ h) = φ⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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