no goals
R : Type ?u.112343
A : Type ?u.112346
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℝ
n : ℕ
⊢ eval (cos θ) (U ℝ n) * sin θ = sin ((↑n + 1) * θ)
exact_mod_cast U_complex_cos θ n