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 997 to 1,002 of 2,569 results.
EoF_of_MES
Mathematical statement
The entanglement of formation of the maximally entangled state with on-site dimension 𝕕 is log(𝕕).
Source project: quantumInfo
Person-level attribution pending.
eq_biUnion_iteratedMaximalSubfamily
Mathematical statement
Any set of tiles can be written as the union of disjoint subfamilies, their number being controlled by the maximal stack size.
Source project: Carleson formalization
Person-level attribution pending.
eq_pow_prime_of_unit_of_congruent
Mathematical statement
A regular prime criterion: if a unit of the cyclotomic field is congruent to an integer modulo p, then it is a p-th power.
Source project: FLT for regular primes
Person-level attribution pending.
Eq1323.Equation1323_not_implies_Equation2744
Mathematical statement
Source project: Equational Theories
Person-level attribution pending.
Eq677.eq255_equiv_LxRx
Mathematical statement
Blueprint Lemma 13.2(v). E255 at x ↔ L_x ∘ R_x has a fixed point.
Source project: Equational Theories
Person-level attribution pending.
equation4
Project documentation
Apply the optional stopping theorem to get equation 4. Note that T1 Space is needed to make sure that mesh ι n has order topology.
Source project: Brownian motion
Person-level attribution pending.