`BookProof.ChapterE4.wave_succ` (θ : ℕ → ℝ) (s d : ℕ) (i : ℕ) : wave θ s (d + 1) i = Real.cos (θ s) * basisVec s i + Real.sin (θ s) * wave θ (s + 1) d i

Initializing...

`BookProof.ChapterE4.wave_succ` (θ : ℕ → ℝ) (s d : ℕ) (i : ℕ) : wave θ s (d + 1) i = Real.cos (θ s) * basisVec s i + Real.sin (θ s) * wave θ (s + 1) d i · Prove2Me