E : Type ?u.12721
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
⊢ c +ᵥ sphere (R • 0) (‖R‖ * 1) = sphere c (Abs.abs R)
E : Type ?u.12721
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
⊢ (c +ᵥ R • range fun θ => exp (↑θ * I)) = sphere c (Abs.abs R)
rw [Complex.range_exp_mul_I, smul_sphere R 0 zero_le_one]
no goals
E : Type ?u.12721
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
⊢ c +ᵥ sphere (R • 0) (‖R‖ * 1) = sphere c (Abs.abs R)
simp