Proof step e-4bbc13aea32d7e48

definition_equality → concludes about Triangle of numbers T(n,k) = k!*Stirling2(n,k) read by rows (n >= 1, 1 <= k <= n). 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 a14ebeed2ef27ee5c0236f76b1d5d6b3d8ea7d1f5fb2dd180bf4b8223c174dd1, 17,086 bytes (3,308 compressed); download JSON