Proof step e-dfb7962499f04eaa

definition_equality → concludes about Infinite lower triangular matrix with 2^k in the right diagonal and the rest zeros. Triangle, T(n,k), n zeros followed by the term 2^k. Triangle by columns, (2… 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 a1ff49d29a81b3fa93cfbd10a92d20316d27d00e63c8d5561d9cdca93fab5703, 4,774 bytes (1,479 compressed); download JSON