{"id":"e-5fb73cf2df09a656","operation":{"operation":"definition_equality"},"operation_detail":null,"conclusion_id":"n-b2f14d9f44a39df2","premise_count":0,"theorem":"all-index identity Q_n = P_n certified by exact Ore-algebra division and identifying rows (polytool preserver-image certificate of the identity map)","lean_route":null,"lean_declarations":[],"certificate_hash":"75af8daaec922482452fc374d6cdc0b550e2466d79a7f314868d37360931709d","verification_polytool":"replayed","verification_lean":"not_attempted","certificate_kind":"definition_equality","certificate_raw_size":10384,"certificate_compressed_size":2808,"conclusion_name":"Triangle of coefficients of Legendre polynomials 2^n P_n (x).","claims":[],"premises":[],"cited_by":[]}