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)
163noncomputable def deltam21_sq : ℝ := 7.42e-5 -- eV²
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.
-
deltam21_sq
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use
-
m2_estimate
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use
-
massRatio
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use
-
mass_ratio_phi4
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use
-
mass_ratio_phi7
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use
-
mass_ratio
in IndisputableMonolith.StandardModel.PMNSMatrix
decl_use
-
mass_ratio_phi_connection
in IndisputableMonolith.StandardModel.PMNSMatrix
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
deltam21_sq
in IndisputableMonolith.StandardModel.NeutrinoMassHierarchy
decl_use