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 865 to 870 of 2,569 results.
det_muller_lang_imp_omega_reg_lang
Mathematical statement
Every deterministic Muller language is an ω-regular language.
Source project: Automata Theory
Person-level attribution pending.
det_muller_lang_inter
Mathematical statement
Deterministic Muller languages are closed under intersection.
Source project: Automata Theory
Person-level attribution pending.
det_muller_lang_union
Mathematical statement
Deterministic Muller languages are closed under union.
Source project: Automata Theory
Person-level attribution pending.
DeterminantBound.application
Mathematical statement
A particular application of the determinant bound used in subcase 2.1
Source project: ABC Exceptions
Person-level attribution pending.
di_in_ff
Project documentation
A finite-field density-increment lemma. If the normalized additive correlation of with a set of density at least differs from its random value by at least , then there is a subspace of explicitly bounded codimension. Averaging over raises its density to at least , where is the density of .
Source project: Arithmetic Progressions Almost Periodicity
Person-level attribution pending.
differentiableAt_jacobiTheta₂_half
Mathematical statement
Differentiability of t ↦ jacobiTheta₂(t/2, t) at points in the upper half-plane.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.