def
definition
def or abbrev
Matches
show as:
view Lean formalization →
formal statement (Lean)
132def Matches (φ : ℝ) (L : Ledger) (B : Bridge L) (U : UniversalDimless φ) : Prop :=
proof body
Definition body.
133 ∃ (P : DimlessPack L B),
134 P.alpha = U.alpha0
135 ∧ P.massRatios = U.massRatios0
136 ∧ P.mixingAngles = U.mixingAngles0
137 ∧ P.g2Muon = U.g2Muon0
138 ∧ P.strongCPNeutral = U.strongCP0
139 ∧ P.eightTickMinimal = U.eightTick0
140 ∧ P.bornRule = U.born0
141
142end
143
144end RecogSpec
145end IndisputableMonolith