Proof step

Ore-algebra identity of two definitions

All-n equality of two definitions

Concludes: shift_x_plus_one of basis_map_A007318 of Riordan array (1/(1-2*x), x*(1+x)/(1-2*x)).
Premises: none: a direct theorem check
Theorem: polytool ?
Checked: polytool replayed · Lean not attempted

Technical details

Step id

e-fdfc0c621074efe4 · JSON

Operation

All-n equality of two definitions

{
  "operation": "definition_equality"
}

Claims

Certificate

definition_equality, SHA-256 6e2ca85f2767bb8d635936ab17c4f1bbf86867bf90d7de3c323812284224934b, 30,322 bytes (5,445 compressed); download

polytool replayed the certificate when the step was written.