Theorem: Section2sheet6.tendsTo_neg' (FormalisingMathematics2024/Section02reals/Sheet6.lean)

State before:
a : ℕ → ℝ
t : ℝ
ha : TendsTo a t
⊢ TendsTo (fun n => -a n) (-t)
Tactic:
simpa using tendsTo_const_mul (-1) ha
State after:
no goals