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 2 research declarations. Search 10,000 more complete Mathlib declarations.
2 results
Clear filtersFieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul
Plain-language statement
In the state algebra time, ordering obeys T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ) where φᵢ is the state which has maximum time and s is the exchange sign of φᵢ and φ₀φ₁…φᵢ₋₁.
Source project: Physlib
Person-level attribution pending.
FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset
Plain-language statement
In the state algebra time, ordering obeys T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ) where φᵢ is the state which has maximum time and s is the exchange sign of φᵢ and φ₀φ₁…φᵢ₋₁. Here s is written using finite sets.
Source project: Physlib
Person-level attribution pending.