def definition def or abbrev

`muon_electron_ratio`

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

formal statement (Lean)

  27noncomputable def muon_electron_ratio : ℝ := φ ^ 11

Definition body.

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

lepton_masses_from_ladder in IndisputableMonolith.Masses.LeptonMassLadder decl_use
muon_electron_ratio in IndisputableMonolith.Masses.LeptonMassLadder decl_use
muon_electron_ratio in IndisputableMonolith.Physics.AnchorPolicy decl_use
muon_heavier in IndisputableMonolith.Physics.ProtonRadius decl_use
muonic_smaller in IndisputableMonolith.Physics.ProtonRadius decl_use
muon_ratio_pos in IndisputableMonolith.Physics.ProtonRadius decl_use

Lean names referenced from this declaration's body.

muon_electron_ratio in IndisputableMonolith.Masses.LeptonMassLadder decl_use
muon_electron_ratio in IndisputableMonolith.Physics.AnchorPolicy decl_use