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

1 topic

18 results

Clear filters

Project-declaredLean 4.32.0

Contr co Contr Unit

Lorentz.contr_coContrUnit

Plain-language statement

Contraction on the right with coContrUnit.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Contr pre Co Contr Unit

Lorentz.contr_preCoContrUnit

Plain-language statement

Contraction on the right with coContrUnit.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Contr pre Contr Co Unit

Lorentz.contr_preContrCoUnit

Plain-language statement

Contraction on the right with contrCoUnit does nothing.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Contr Co Contraction apply metric

Lorentz.contrCoContraction_apply_metric

Project documentation

The metric ηᵢᵢ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo, making its invariance under the action of SL(2,ℂ). -/ def coMetric : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap (CoℂModule.SL2CRep.tprod CoℂModule.SL2CRep) where toFun := fun a => let a' : ℂ := a a' • coMetricVal map_add' := fun x y => by simp only [add_smul] map_smu...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0