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

1 topic

15 results

Clear filters
Project-declaredLean 4.32.0

Reduce num Chiral U of mem elems No Exotics

FTheory.SU5.TenQuanta.reduce_numChiralU_of_mem_elemsNoExotics

Project documentation

The reduce of TenQuanta is a new TenQuanta with all the fluxes corresponding to the same charge (i.e. representation) added together. -/ def reduce (x : TenQuanta 𝓩) : TenQuanta 𝓩 := x.toCharges.dedup.map fun q10 => (q10, ((x.filter (fun f => f.1 = q10)).map (fun y => y.2)).sum) /-! ### B.1. The reduced TenQuanta has no duplicate elements -/ lem...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Reduce sum eq sum to Charges

FTheory.SU5.TenQuanta.reduce_sum_eq_sum_toCharges

Project documentation

The reduce of TenQuanta is a new TenQuanta with all the fluxes corresponding to the same charge (i.e. representation) added together. -/ def reduce (x : TenQuanta 𝓩) : TenQuanta 𝓩 := x.toCharges.dedup.map fun q10 => (q10, ((x.filter (fun f => f.1 = q10)).map (fun y => y.2)).sum) /-! ### B.1. The reduced TenQuanta has no duplicate elements -/ lem...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

To Charge to Finset of mem lift Charge

FTheory.SU5.TenQuanta.toCharge_toFinset_of_mem_liftCharge

Project documentation

Given a finite set of charges c the TenQuanta which do not have exotics, duplicate charges or zero fluxes, which map down to c. This is defined to be as efficient as possible. -/ def liftCharge (c : Finset 𝓩) : Multiset (TenQuanta 𝓩) := /- The {(1, 0), (1, 0), (1, 0)} case. -/ /- The multisets of cardinality 3 containing 3 elements of c. -/ let...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record