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

Apply eq sum even term Of Mass Dim

StandardModel.HiggsField.EffectivePotential.apply_eq_sum_even_termOfMassDim

Project documentation

The part of a potential at a given mass-dimension. -/ def termOfMassDim (V : EffectivePotential) {n : ā„•} (h : HasMaxMassDimLE V n) (m : ā„•) : HiggsVec ā†’ ā„ := fun Ļ† => ((polynomial V h).homogeneousComponent m).eval Ļ†.toRealScalars lemma termOfMassDim_eq_zero_of_max_lt {V : EffectivePotential} {n : ā„•} (h : HasMaxMassDimLE V n) {m : ā„•} (hm : n < m) (Ļ† : Higgs...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record