invOfUnit_eq' — Mathlib

English

If φ ∈ k[[X]] and u ∈ Units k satisfy constantCoeff φ = u, then invOfUnit φ u = φ⁻¹.

Русский

Пусть φ ∈ k[[X]] и u ∈ U(k) удовлетворяют равенству constantCoeff φ = u; тогда invOfUnit φ u = φ⁻¹.

LaTeX

$$$$ \operatorname{constantCoeff}(\phi) = u \quad\Rightarrow\quad \operatorname{invOfUnit}(\phi, u) = \phi^{-1}. $$$$

Lean4

@[simp]
theorem invOfUnit_eq' (φ : k⟦X⟧) (u : Units k) (h : constantCoeff φ = u) : invOfUnit φ u = φ⁻¹ :=
  MvPowerSeries.invOfUnit_eq' φ _ h

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