Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 667 to 672 of 2,569 results.
Cslib.SKI.isBool_injective
Mathematical statement
Injectivity for booleans.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.isChurch_injective
Mathematical statement
Injectivity for Church numerals
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.List.headD_correct
Mathematical statement
General head-with-default correctness.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.parallelReduction_diamond
Mathematical statement
The key result: the Church-Rosser property holds for ⭢ₚ. The proof is a lengthy case analysis on the reductions a ⭢ₚ a₁ and a ⭢ₚ a₂, but is entirely mechanical.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.Polynomial.elimVar_correct
Mathematical statement
Correctness for the elimVar algorithm, which provides the inductive step of the bracket abstraction algorithm. We induct backwards on the list, corresponding to applying the transformation from the inside out. Since we haven't defined reduction for polynomials, we substitute arbitrary terms for the inner variables.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.SKI.Polynomial.toSKI_correct
Mathematical statement
Correctness for the toSKI (bracket abstraction) algorithm.
Source project: Lean Computer Science Library
Person-level attribution pending.