order_neg — Mathlib

English

The order of the negation of a power series equals the order of the original series.

Русский

Порядок отрицания степенного ряда равен порядку исходного ряда.

LaTeX

$$$\operatorname{order}(-\phi) = \operatorname{order}(\phi)$$$

Lean4

@[simp]
theorem order_neg {R : Type*} [Ring R] (φ : PowerSeries R) : (-φ).order = φ.order :=
  by
  by_contra! h
  have : φ = 0 := by simpa using (order_add_of_order_ne _ _ h).symm
  simp [this] at h

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