`BookProof.ChapterLegendrePolynomial.legendreAux_ode` (l : ℕ) : (X ^ 2 - 1) * derivative^[2] (legendreAux l) + C 2 * X * derivative (legendreAux l)

Initializing...

`BookProof.ChapterLegendrePolynomial.legendreAux_ode` (l : ℕ) : (X ^ 2 - 1) * derivative^[2] (legendreAux l) + C 2 * X * derivative (legendreAux l) - C ((l : ℝ) * ((l : ℝ) + 1)) * · Prove2Me