order_zero_of_unit — Mathlib

English

If a formal power series f is invertible, then its order is 0.

Русский

Если ряд f инвертируем, то его порядок равен 0.

LaTeX

$$IsUnit(f) \Rightarrow f.order = 0$$

Lean4

/-- The order of an invertible power series is `0`. -/
theorem order_zero_of_unit {f : R⟦X⟧} : IsUnit f → f.order = 0 :=
  by
  rintro ⟨⟨u, v, hu, hv⟩, hf⟩
  apply And.left
  rw [← add_eq_zero, ← hf, ← nonpos_iff_eq_zero, ← @order_one R _ _, ← hu]
  exact order_mul_ge _ _

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