Proof step e-e62cfe3f46e65c48
definition_equality → concludes about basis_map_A007318 of Triangle read by rows: T(k,s) = ((2*k+1)/(2*s+1))*binomial(k+s,2*s), 0 <= s <= k. JSON
Theorem
Ore-algebra identity of two definitions polytool ?
Operation
All-n equality of two definitions
{
"operation": "definition_equality"
}
Premises
None: this step is a direct theorem check.
Claims
Verification and certificate
- polytool: replayed (the certificate replayed when the step was written)
- Lean: not attempted
- certificate:
definition_equality, SHA-256e30f127c1df34da9d7ed5de098846eecacc2a7ef9fa4882b5ec26c0ae410e30c, 18,147 bytes (3,603 compressed); download JSON