def
definition
def or abbrev
sin2_theta12_observed
show as:
view Lean formalization →
formal statement (Lean)
45noncomputable def sin2_theta12_observed : ℝ := 0.307
proof body
Definition body.
46
47/-- The atmospheric mixing angle θ₂₃ ≈ 49° (sin²θ₂₃ ≈ 0.545). -/