Proof step

Ore-algebra identity of two definitions

All-n equality of two definitions

Concludes: shift_x_plus_one of Triangle read by rows: T(n,k) = C(n+k,n)*C(n,k)/(k+1), for n >= 0, k = 0..n.
Premises: none: a direct theorem check
Theorem: polytool ?
Checked: polytool replayed · Lean not attempted

Technical details

Step id

e-907ff3ac724c18dd · JSON

Operation

All-n equality of two definitions

{
  "operation": "definition_equality"
}

Claims

Certificate

definition_equality, SHA-256 f67130aa94047df16c0fff2c11f26681d9cd1d57b19bdcadc347707bd85c62bb, 19,843 bytes (3,734 compressed); download

polytool replayed the certificate when the step was written.