therefore
Sign up
Open navigation

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

Super Commute F grade

FieldSpecification.FieldOpFreeAlgebra.superCommuteF_grade

Project documentation

For a field specification 𝓕, and two lists Ο†s = φ₀…φₙ and Ο†s' of 𝓕.CrAnFieldOp the following super commutation relation holds: [Ο†s', φ₀…φₙ]β‚›F = βˆ‘ i, 𝓒(Ο†s', φ₀…φᡒ₋₁) β€’ φ₀…φᡒ₋₁ * [Ο†s', Ο†α΅’]β‚›F * Ο†α΅’β‚Šβ‚ … Ο†β‚™ The proof of this relation is via induction on the length of Ο†s. -/ lemma superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum (Ο†s : List 𝓕.CrAnFiel...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Super Commute F of Cr An List F of Cr An List F cons

FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_cons

Plain-language statement

For a field specification 𝓕, the super commutator superCommuteF is defined as the linear map 𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra which on the lists Ο†s and Ο†s' of 𝓕.CrAnFieldOp gives superCommuteF Ο†s Ο†s' = Ο†s * Ο†s' - 𝓒(Ο†s, Ο†s') β€’ Ο†s' * Ο†s. The notation [a, b]β‚›F can be used for superCommuteF a b...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record