def definition def or abbrev

`ratio_mu_e_exp`

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

formal statement (Lean)

 165noncomputable def ratio_mu_e_exp : ℝ := m_mu_exp / m_e_exp

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

ChargedLeptonMassScoreCardCert in IndisputableMonolith.Masses.ChargedLeptonMassScoreCard decl_use
row_muon_electron_ratio in IndisputableMonolith.Masses.ChargedLeptonMassScoreCard decl_use
row_muon_electron_ratio_pct in IndisputableMonolith.Masses.QuarkScoreCard decl_use
MassVerificationCert in IndisputableMonolith.Masses.Verification decl_use
muon_electron_ratio_error in IndisputableMonolith.Masses.Verification decl_use
muon_ratio_undershoot in IndisputableMonolith.Masses.Verification decl_use
ratio_mu_e_exp_bounds in IndisputableMonolith.Masses.Verification decl_use

Lean names referenced from this declaration's body.