structure
definition
def or abbrev
ThetaQCD
show as:
view Lean formalization →
formal statement (Lean)
48structure ThetaQCD where
49 value : ℝ
50 in_range : 0 ≤ value ∧ value < 2 * π
51
52/-- The experimental bound on |θ|:
53 From the neutron electric dipole moment (EDM).
54 d_n < 10⁻²⁶ e·cm implies |θ| < 10⁻¹⁰ -/