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 136 research declarations. Search 10,000 more complete Mathlib declarations.
136 results
Clear filtersCslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.reconstruct_eq_constantCoeff_of_eval_eq
Plain-language statement
Reconstruction recovers the constant coefficient of any low-degree polynomial from its values at distinct points.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.SecretSharing.Shamir.view_indist_of_tailSampler
Plain-language statement
Translation-invariant Shamir tail samplers induce secret-independent views for unauthorized coalitions.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.AdmissibleRun.fault_zero
Plain-language statement
Specialize the definition of Algorithm.AdmissibleRun to the case of zero fault.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.Algorithm.omega_notRcvd_enabled
Plain-language statement
A message that is in-flight stays in-flight as long as it is not received (infinite execution version).
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.Algorithm.recvMsg_comm
Plain-language statement
If m1 and m2 are both inflight and they have different destinations, then receiving them in either order produces the same end state.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.Algorithm.tr_diamond
Plain-language statement
A diamond property for the transition relation a.lts.Tr.
Source project: Lean Computer Science Library
Person-level attribution pending.