Proof step
Ore-algebra identity of two definitions
All-n equality of two definitions
- Concludes
- shift_x_plus_one of 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, …
- Premises
- none: a direct theorem check
- Theorem
- polytool ?
- Checked
- polytool replayed · Lean not attempted
Technical details
- Step id
e-b1b3df86c56d48cf· JSON- Operation
- All-n equality of two definitions
{ "operation": "definition_equality" } - Claims
- Certificate
definition_equality, SHA-2567627d37acad7fc67c22abd710687d58a3e4e02dbd41005329f16c81d7534bfdf, 30,671 bytes (5,798 compressed); downloadpolytool replayed the certificate when the step was written.