English
Scaling by a nonzero scalar c preserves radius: (c•p).radius = p.radius.
Русский
Умножение на ненулевой скаляр сохраняет радиус.
LaTeX
$$$\\text{If } c \\neq 0:\\quad (c\\cdot p).radius = p.radius.$$$
Lean4
theorem exists_hasSum_smul_of_apply_eq_zero (hs : HasSum (fun m => z ^ m • a m) s) (ha : ∀ k < n, a k = 0) :
∃ t : E, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t :=
by
obtain rfl | hn := n.eq_zero_or_pos
· simpa
by_cases h : z = 0
· have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using hasSum_at_zero a)
exact ⟨a n, by simp [h, hn.ne', this], by simpa [h] using hasSum_at_zero fun m => a (m + n)⟩
· refine ⟨(z ^ n)⁻¹ • s, by match_scalars; field_simp, ?_⟩
have h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0 :=
Finset.sum_eq_zero fun k hk => by simp [ha k (Finset.mem_range.mp hk)]
have h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s := by simpa [h1] using (hasSum_nat_add_iff' n).mpr hs
convert h2.const_smul (z⁻¹ ^ n) using 2 with x
· match_scalars
simp [field, pow_add]
· simp only [inv_pow]
