Proof step
Ore-algebra identity of two definitions
All-n equality of two definitions
- Concludes
- shift_x_plus_one of Triangle of coefficients of Legendre polynomials 2^n P_n (x).
- Premises
- none: a direct theorem check
- Theorem
- polytool ?
- Checked
- polytool replayed · Lean not attempted
Technical details
- Step id
e-10d7d1201ce81550· JSON- Operation
- All-n equality of two definitions
{ "operation": "definition_equality" } - Claims
- Certificate
definition_equality, SHA-25620e7816e6881caf7ae1fa6409b2f8ef0cf4b3431203af6c862a4a4e91881a4a1, 28,119 bytes (5,004 compressed); downloadpolytool replayed the certificate when the step was written.