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 565 to 570 of 2,569 results.
CoreResults.vecMul_injective_of_rank_eq
Mathematical statement
If G has full row rank, then every nonzero vector maps to a nonzero codeword.
Source project: ArkLib
Person-level attribution pending.
count_not
Mathematical statement
count of the negative of f
Source project: debate
Person-level attribution pending.
CPTPMap.id_achievesRate_log_dim
Mathematical statement
The identity channel on D dimensional space achieves a rate of log2(D).
Source project: quantumInfo
Person-level attribution pending.
CPTPMap.not_achievesRate_gt_log_dim_out
Mathematical statement
A channel cannot achieve a rate greater than log2(D), where D is the output dimension.
Source project: quantumInfo
Person-level attribution pending.
Cslib.Automata.DA.FinAcc.unique_minimal
Mathematical statement
The minimal DFA M accepting the language l is unique up to unique isomorphism.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.buchiFamily_cover
Project documentation
na.buchiFamily is a cover if na has only finitely many states. This theorem uses the Ramsey theorem for infinite graphs and does not depend on any details of na.BuchiCongruence other than that it is of finite index.
Source project: Lean Computer Science Library
Person-level attribution pending.