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)
35def m_d_contrib : ℝ := mass_on_rung 4
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
-
binding_dominates
in IndisputableMonolith.StandardModel.ProtonMass
decl_use
-
m_valence
in IndisputableMonolith.StandardModel.ProtonMass
decl_use
-
m_valence_pos
in IndisputableMonolith.StandardModel.ProtonMass
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
mass_on_rung
in IndisputableMonolith.Masses.MassHierarchy
decl_use