no goals
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
⊢ eval (cos θ) (T ℂ 0) = cos (↑0 * θ)
simp only [T_zero, eval_one, Nat.cast_zero, MulZeroClass.zero_mul, cos_zero]
no goals
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
⊢ eval (cos θ) (T ℂ 1) = cos (↑1 * θ)
simp only [eval_X, one_mul, T_one, Nat.cast_one]
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ eval (cos θ) (T ℂ (n + 2)) = cos (↑(n + 2) * θ)
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
⊢ eval (cos θ) (T ℂ (n + 2)) = cos (↑(n + 2) * θ)
have : (2 : ℂ[X]) = (2 : ℕ) := by norm_num
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ ↑2 * cos θ * eval (cos θ) (T ℂ (n + 1)) - eval (cos θ) (T ℂ n) = cos (↑(n + 2) * θ)
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ eval (cos θ) (T ℂ (n + 2)) = cos (↑(n + 2) * θ)
simp only [this, eval_X, eval_one, T_add_two, eval_sub, eval_mul, eval_nat_cast]
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * cos θ * eval (cos θ) (T ℂ (n + 1)) - eval (cos θ) (T ℂ n) = cos ((↑n + 2) * θ)
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ ↑2 * cos θ * eval (cos θ) (T ℂ (n + 1)) - eval (cos θ) (T ℂ n) = cos (↑(n + 2) * θ)
simp only [Nat.cast_ofNat, Nat.cast_add]
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * cos θ * cos (↑(n + 1) * θ) - cos (↑n * θ) = cos ((↑n + 2) * θ)
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * cos θ * eval (cos θ) (T ℂ (n + 1)) - eval (cos θ) (T ℂ n) = cos ((↑n + 2) * θ)
rw [T_complex_cos (n + 1), T_complex_cos n]
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * (cos θ * (cos (↑n * θ) * cos θ - sin (↑n * θ) * sin θ)) - cos (↑n * θ) =
    cos (↑n * θ) * (2 * cos θ ^ 2 - 1) - sin (↑n * θ) * (2 * (sin θ * cos θ))
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * cos θ * cos (↑(n + 1) * θ) - cos (↑n * θ) = cos ((↑n + 2) * θ)
simp only [Nat.cast_add, Nat.cast_one, add_mul, cos_add, one_mul, mul_assoc, sin_two_mul,
  cos_two_mul]
no goals
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * (cos θ * (cos (↑n * θ) * cos θ - sin (↑n * θ) * sin θ)) - cos (↑n * θ) =
    cos (↑n * θ) * (2 * cos θ ^ 2 - 1) - sin (↑n * θ) * (2 * (sin θ * cos θ))
ring
no goals
R : Type ?u.105956
A : Type ?u.105959
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
⊢ 2 = ↑2
norm_num