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

All topics

591 results

Clear filters
Project-declaredLean 4.32.0

Euclid Levi Civita symbol contract zero

euclidLeviCivita_symbol_contract_zero

Plain-language statement

Full Euclidean Levi-Civita contraction ∑_b (ε4)_b · (ε4)_b = 24 at the symbol level: summing the square of every standard-basis component of ε4 over all four Fin 4 index slots, paired naively (no metric), counts the 4! = 24 permutations. The Lorentz contraction ε^{μνρσ} ε_{μνρσ} lowers one factor with η and equals -24 instead.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Comm metric Raw

Fermion.comm_metricRaw

Plain-language statement

Multiplying an element of SL(2, ℂ) on the left with the metric 𝓔 is equivalent to multiplying the inverse-transpose of that element on the right with the metric.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Contr dual Left Left Unit

Fermion.contr_dualLeftLeftUnit

Plain-language statement

Contraction on the right with dualLeftLeftUnit does nothing.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Contr dual Right Right Unit

Fermion.contr_dualRightRightUnit

Plain-language statement

Contraction on the right with dualRightRightUnit does nothing.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Contr left Dual Left Unit

Fermion.contr_leftDualLeftUnit

Plain-language statement

Contraction on the right with leftDualLeftUnit does nothing.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Contr right Dual Right Unit

Fermion.contr_rightDualRightUnit

Plain-language statement

Contraction on the right with rightDualRightUnit does nothing.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record