Proof step
Ore-algebra identity of two definitions
All-n equality of two definitions
- Concludes
- Triangle T(n,k) read by rows: associated Stirling numbers of first kind (n >= 2, 1 <= k <= floor(n/2)).
- Premises
- none: a direct theorem check
- Theorem
- polytool ?
- Checked
- polytool replayed · Lean not attempted
Technical details
- Step id
e-2bf4ffda16430b0b· JSON- Operation
- All-n equality of two definitions
{ "operation": "definition_equality" } - Claims
- Certificate
definition_equality, SHA-2565d3265d1c7f0d15e2bb3c86832d0dd7cd0731f7a9205b9de5a2ae3768cc061f0, 7,909 bytes (2,338 compressed); downloadpolytool replayed the certificate when the step was written.