Theorem: Section2sheet6Solutions.tendsTo_mul_const (FormalisingMathematics2024/Solutions/Section02reals/Sheet6.lean)

State before:
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => a n * c) (t * c)
Tactic:
simpa [mul_comm] using tendsTo_const_mul c h
State after:
no goals