Proof step e-9288cdb19cf0727b

definition_equality → concludes about basis_map_A007318 of Triangle T(n,k), 0 <= k <= n, read by rows, given by [1,0,-1,0,0,0,0,0,0,...] DELTA [3,-2,-1,0,0,0,0,0,0,...] where DELTA is the operator … 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-256 9e96ab175d2a3caa9fd8bca780a38d87c3c9302f03c55a52f7620e29caf39b2f, 7,431 bytes (2,326 compressed); download JSON