inv_eq_zero — Mathlib

English

φ⁻¹ = 0 if and only if constantCoeff φ = 0.

Русский

φ⁻¹ = 0 тогда и только тогда, когда constantCoeff φ = 0.

LaTeX

$$$ φ^{-1} = 0 \iff constantCoeff(φ) = 0 $$$

Lean4

theorem inv_eq_zero {φ : MvPowerSeries σ k} : φ⁻¹ = 0 ↔ constantCoeff φ = 0 :=
  ⟨fun h => by simpa using congr_arg constantCoeff h, fun h =>
    ext fun n => by
      classical
      rw [coeff_inv]
      split_ifs <;> simp only [h, map_zero, zero_mul, inv_zero, neg_zero]⟩

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