`BookProof.ChapterLegendrePolynomial.legendre_deriv_coeff_eq_zero` (l μ k : ℕ) (h : l < k + μ) : (derivative^[μ] (legendre l)).coeff k = 0

Initializing...

`BookProof.ChapterLegendrePolynomial.legendre_deriv_coeff_eq_zero` (l μ k : ℕ) (h : l < k + μ) : (derivative^[μ] (legendre l)).coeff k = 0 · Prove2Me