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 1,525 to 1,530 of 2,569 results.
Language.dfa_num_state_min
Mathematical statement
All DFAs accepting l must have at least as many states as the number of equivalence classes of the Nerode congruence on l.
Source project: Lean Computer Science Library
Person-level attribution pending.
Language.IsRegular.finite_nerodeQuotient
Mathematical statement
If l is regular then the Nerode congruence on l has finitely many equivalence classes.
Source project: Lean Computer Science Library
Person-level attribution pending.
Language.kstar_sub_one
Mathematical statement
A grind regression found moving to nightly-2026-03-31 (changes from lean#13166)
Source project: Lean Computer Science Library
Person-level attribution pending.
Language.sub_one_mul
Mathematical statement
A grind regression found moving to nightly-2026-03-31 (changes from lean#13166)
Source project: Lean Computer Science Library
Person-level attribution pending.
le_CarlesonOperatorReal
Mathematical statement
For and an interval-integrable function , the norm of the localized Dirichlet-kernel integral over , with cutoff , is bounded by the sum of the real Carleson operators applied to and to its complex conjugate.
Source project: Carleson formalization
Person-level attribution pending.
le_liminf_of_eventually_monotone_of_tendsto_on_dense
Mathematical statement
This is the dual of limsup_le_of_eventually_monotone_of_tendsto_on_dense.
Source project: Brownian motion
Person-level attribution pending.