inv_mul_cancel — Mathlib

English

Similarly, φ⁻¹ · φ = 1 and φ · φ⁻¹ = 1 under suitable conditions; the symmetry of inverse in mv power series.

Русский

Аналогично, при соответствующих условиях, φ⁻¹ · φ = 1 и φ · φ⁻¹ = 1; симметрия обратной в mv степенных рядах.

LaTeX

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

Lean4

@[simp]
protected theorem inv_mul_cancel (φ : MvPowerSeries σ k) (h : constantCoeff φ ≠ 0) : φ⁻¹ * φ = 1 := by
  rw [mul_comm, φ.mul_inv_cancel h]

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