`BookProof.ChapterLegendrePolynomial.legendre_coeff_eq_zero_of_lt` (l k : ℕ) (h : l < k) : (legendre l).coeff k = 0

Initializing...

`BookProof.ChapterLegendrePolynomial.legendre_coeff_eq_zero_of_lt` (l k : ℕ) (h : l < k) : (legendre l).coeff k = 0 · Prove2Me