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.CCS.Context.complete
Plain-language statement
Any Process can be obtained by filling a Context with an atom. This proves that Context is a complete formalisation of syntactic contexts for CCS.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Computability.Turing.SingleTape.SingleTapeNTM.mYields_mTr
Plain-language statement
Characterisation of executions in terms of multistep transitions.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.PerfectSecrecy.ciphertextIndist_of_perfectlySecret
Plain-language statement
Perfect secrecy implies ciphertext indistinguishability.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.PerfectSecrecy.perfectlySecret_iff_indep
Plain-language statement
Perfect secrecy is equivalent to message-ciphertext independence. The two formulations are related by multiplying/dividing by marginal(c).
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.PerfectSecrecy.shannonKeySpace
Project documentation
Perfect secrecy requires |K| ≥ |M| (Shannon's theorem).
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.natDegree_sharingPolynomial_le
Plain-language statement
If the tail polynomial has degree < n, then the sharing polynomial has natural degree at most n.
Source project: Lean Computer Science Library
Person-level attribution pending.