pith. machine review for the scientific record. sign in
structure definition def or abbrev

UniversalDimless

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 118structure UniversalDimless (φ : ℝ) : Type where
 119  alpha0        : ℝ
 120  massRatios0   : LeptonMassRatios
 121  mixingAngles0 : CkmMixingAngles
 122  g2Muon0       : ℝ
 123  strongCP0     : Prop
 124  eightTick0    : Prop
 125  born0         : Prop
 126  alpha0_isPhi        : PhiClosed φ alpha0
 127  massRatios0_isPhi   : massRatios0.Forall (PhiClosed φ)
 128  mixingAngles0_isPhi : mixingAngles0.Forall (PhiClosed φ)
 129  g2Muon0_isPhi       : PhiClosed φ g2Muon0
 130
 131/-- "Bridge B matches universal U" (pure proposition). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.