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

1 topic

1 result

Clear filters
Project-declaredLean 4.32.0

Uncontracted List succ Above Emb erase Idx to Finset

WickContraction.uncontractedList_succAboveEmb_eraseIdx_toFinset

Project documentation

The embedding of Fin [Ļ†sĪ›]įµ˜į¶œ.length into Fin Ļ†s.length. -/ def uncontractedListEmd {Ļ†s : List š“•.FieldOp} {Ļ†sĪ› : WickContraction Ļ†s.length} : Fin [Ļ†sĪ›]įµ˜į¶œ.length ā†Ŗ Fin Ļ†s.length := ((finCongr (by simp [uncontractedListGet])).trans Ļ†sĪ›.uncontractedIndexEquiv).toEmbedding.trans (Function.Embedding.subtype fun x => x āˆˆ Ļ†sĪ›.uncontracted) lemma uncontracted...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record