Proof step e-5f2e71a1e47d5fe3
definition_equality → concludes about Triangle of Narayana numbers T(n,k) = C(n-1,k-1)*C(n,k-1)/k with 1 <= k <= n, read by rows. Also called the Catalan triangle. 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-2568cf6162eb8c6172d737f778d31a5dfac753ed799769f4cd075771a6c9af91f1c, 16,152 bytes (3,689 compressed); download JSON