Proof step e-7c5de25572de6f9f
definition_equality → concludes about basis_map_A007318 of Triangle T(n, k) is coefficient of z^n*w^k in 1/(1 - 2*z - 2*w - 2*z*w) read by rows in order 00, 10, 01, 20, 11, 02, ... 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-256904ab8390d12632694af7d4de9875047e10179f6bc9f10c3b25db75f168ae6d5, 15,161 bytes (3,966 compressed); download JSON