mul_inv_cancel — Mathlib

English

φ⁻¹ · φ = 1 when constantCoeff φ ≠ 0; this follows from invOfUnit and previous lemmas.

Русский

φ⁻¹ · φ = 1 при константном коэффициенте φ ≠ 0; следует из invOfUnit и предыдущих лемм.

LaTeX

$$$ φ^{-1} \cdot φ = 1 $$$

Lean4

@[simp]
protected theorem mul_inv_cancel (φ : MvPowerSeries σ k) (h : constantCoeff φ ≠ 0) : φ * φ⁻¹ = 1 := by
  rw [← invOfUnit_eq φ h, mul_invOfUnit φ (Units.mk0 _ h) rfl]

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