Proof step e-d3b7ddfd0f1aef36
definition_equality → concludes about Irregular triangle read by rows: T(n,k) = binomial(n-k, k), n >= 0, 0 <= k <= floor(n/2); or, coefficients of (one version of) Fibonacci polynomials. 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-256724f411d2412f21e1f7ef9faef3714d401b088da4d43ee9677389fe0a45c3fc0, 6,708 bytes (2,036 compressed); download JSON