`BookProof.ChapterLegendrePolynomial.legendreAux_coeff_self` (l : ℕ) : (legendreAux l).coeff l = ((2 * l).descFactorial l : ℝ)

Initializing...

`BookProof.ChapterLegendrePolynomial.legendreAux_coeff_self` (l : ℕ) : (legendreAux l).coeff l = ((2 * l).descFactorial l : ℝ) · Prove2Me