def definition def or abbrev

`m_p`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  78def m_p : ℝ := m_valence + E_binding

Definition body.

From the project-wide theorem graph. These declarations reference this one in their body.

electron_muon_ratio_uncertainty in IndisputableMonolith.Constants.ExternalAnchors decl_use
muon_mass_MeV in IndisputableMonolith.Constants.ExternalAnchors decl_use
proton_mass_MeV_pos in IndisputableMonolith.Constants.ExternalAnchors decl_use
mass_ratio_structural in IndisputableMonolith.Constants.ProtonElectronMassRatio decl_use
m_e in IndisputableMonolith.Constants.ProtonElectronMassRatio decl_use
proton_electron_ratio_from_ladder in IndisputableMonolith.Constants.ProtonElectronMassRatio decl_use
proton_electron_ratio_implies_phi_gap in IndisputableMonolith.Constants.ProtonElectronMassRatio decl_use
gamow_energy_increases_with_T in IndisputableMonolith.Physics.StellarEvolution decl_use
virial_temperature in IndisputableMonolith.Physics.StellarEvolution decl_use
lambda_qcd_scale in IndisputableMonolith.QFT.RunningCouplings decl_use
landauPoleDescription in IndisputableMonolith.QFT.RunningCouplings decl_use
summary in IndisputableMonolith.QFT.RunningCouplings decl_use
m_p_pos in IndisputableMonolith.StandardModel.ProtonMass decl_use

Lean names referenced from this declaration's body.