neg — Mathlib

English

If a finite formal power-series on a ball exists for f, then it also exists for its negation -f with the negated data.

Русский

Если существует конечная формальная мощносерия на шаре для f, то существует и для его отрицания -f с отрицательными данными.

LaTeX

$$HasFiniteFPowerSeriesOnBall f pf x n r \Rightarrow HasFiniteFPowerSeriesOnBall (-f) (-pf) x n$$

Lean4

theorem neg (hf : HasFiniteFPowerSeriesOnBall f pf x n r) : HasFiniteFPowerSeriesOnBall (-f) (-pf) x n r :=
  ⟨hf.1.neg, fun m hm ↦ by rw [Pi.neg_apply, hf.finite m hm, neg_zero]⟩

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