`BookProof.ChapterEulerCountableChain.stickProb_euler` (θ : ℕ → ℝ) (n : ℕ) : stickProb (condCos θ) n = (∏ k ∈ Finset.range n, Real.sin (θ k) ^ 2) * Real.cos (θ n) ^ 2

Initializing...

`BookProof.ChapterEulerCountableChain.stickProb_euler` (θ : ℕ → ℝ) (n : ℕ) : stickProb (condCos θ) n = (∏ k ∈ Finset.range n, Real.sin (θ k) ^ 2) * Real.cos (θ n) ^ 2 · Prove2Me