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 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

2 results

Clear filters

Project-declaredLean 4.32.0

Insert And Contract snd Field Of Contract some incl

WickContraction.insertAndContract_sndFieldOfContract_some_incl

Plain-language statement

Given a Wick contraction φsΛ for a list φs of 𝓕.FieldOp, an element φ of 𝓕.FieldOp, an i ≤ φs.length and a k in Option φsΛ.uncontracted i.e. is either none or some element of φsΛ.uncontracted, the new Wick contraction φsΛ.insertAndContract φ i k is defined by inserting φ into φs after the first i-elements and moving the value...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Insert And Contract uncontracted List none map

WickContraction.insertAndContract_uncontractedList_none_map

Plain-language statement

For a list φs of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp and a i ≤ φs.length then a sum over Wick contractions of φs with φ inserted at i is equal to the sum over Wick contractions φsΛ of just φs and the sum over optional uncontracted elements of the φsΛ. In other words, `∑ (φsΛ : WickContraction (φs....

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record