invOfUnit_eq' — Mathlib

English

For φ, u ∈ Units k with constantCoeff φ = u, invOfUnit φ u = φ⁻¹.

Русский

Для φ и u ∈ Units k с константным коэффициентом φ = u, invOfUnit φ u = φ⁻¹.

LaTeX

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

Lean4

@[simp]
theorem invOfUnit_eq' (φ : MvPowerSeries σ k) (u : Units k) (h : constantCoeff φ = u) : invOfUnit φ u = φ⁻¹ :=
  by
  rw [← invOfUnit_eq φ (h.symm ▸ u.ne_zero)]
  apply congrArg (invOfUnit φ)
  rw [Units.ext_iff]
  exact h.symm

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