Source-pinned research

Research proof index

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.

All topics

Showing 1,111 to 1,116 of 2,569 results.

Project-declaredLean 4.32.0

Time Order of Field Op List eq Time Only

FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly

Mathematical statement

For a list φs of 𝓕.FieldOp, then 𝓣(φs) = ∑ φsΛ, φsΛ.sign • φsΛ.timeContract * 𝓣(𝓝([φsΛ]ᵘᶜ)) where the sum is over all Wick contraction φsΛ which only have equal time contractions. This result follows from - static_wick_theorem to rewrite 𝓣(φs) on the left hand side as a sum of 𝓣(φsΛ.staticWickTerm). - `EqTimeOnly.timeOrder_staticContra...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Dappend eq add Cases

Fin.dappend_eq_addCases

Mathematical statement

dappend is equal to addCases. Marked as csimp to allow for switching to the addCases implementation during execution.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Drop add Cases right

Fin.drop_addCases_right

Mathematical statement

Dropping the first n + m elements of an addCases u v, where v is a n'-tuple and m ≤ n', is the same as dropping the first m elements of v.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0