invOfUnit_mul — Mathlib

English

If φ has constantCoeff φ = u, then invOfUnit φ u · φ = 1.

Русский

Если константный коэффициент φ равен u, то invOfUnit φ u · φ = 1.

LaTeX

$$$ \mathrm{invOfUnit}(φ, u) \cdot φ = 1 $$$

Lean4

@[simp]
theorem invOfUnit_mul (φ : MvPowerSeries σ R) (u : Rˣ) (h : constantCoeff φ = u) : invOfUnit φ u * φ = 1 :=
  by
  rw [← mul_cancel_right_mem_nonZeroDivisors (r := φ.invOfUnit u), mul_assoc, one_mul, mul_invOfUnit _ _ h, mul_one]
  apply mem_nonZeroDivisors_of_constantCoeff
  simp only [constantCoeff_invOfUnit, IsUnit.mem_nonZeroDivisors (Units.isUnit u⁻¹)]

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