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 44 research declarations. Search 10,000 more complete Mathlib declarations.
44 results
Clear filtersFieldSpecification.WickAlgebra.ofFieldOpList_normalOrder_insert
Plain-language statement
Within a proto-operator algebra, N(φφ₀φ₁…φₙ) = s • N(φ₀…φₖ₋₁φφₖ…φₙ), where s is the exchange sign for φ and φ₀…φₖ₋₁.
Source project: Physlib
Person-level attribution pending.
Fin.dappend_eq_addCases
Plain-language statement
dappend is equal to addCases. Marked as csimp to allow for switching to the addCases implementation during execution.
Source project: ArkLib
Person-level attribution pending.
Fin.happend_heq_right
Plain-language statement
Access into a heterogeneous append on the right, by value: if m ≤ ↑j, then happend u v j is (heterogeneously) the (↑j - m)-th entry of v.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.almost_johnson_choose_2_elimed
Plain-language statement
choose_2-free form of almost_johnson.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.almost_johnson_lhs_div_B_card
Plain-language statement
LHS of the almost-Johnson bound divided by |B| in terms of e and d.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.d_eq_sum
Plain-language statement
The average distance d expressed as a double sum of coordinate disagreements.
Source project: ArkLib
Person-level attribution pending.