abbrev definition def or abbrev

`r_lepton`

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

formal statement (Lean)

  88abbrev r_lepton := Integers.r_lepton

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

m_e_rs in IndisputableMonolith.Constants.ElectronMass decl_use
mass_ratio_geometric in IndisputableMonolith.Foundation.HierarchyDissolution decl_use
r_lepton in IndisputableMonolith.Masses.Anchor decl_use
r_lepton_values in IndisputableMonolith.Masses.Anchor decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung_sdgt in IndisputableMonolith.Masses.AnchorPolicy decl_use
lepton_baseline_matches_anchor in IndisputableMonolith.Masses.BaselineDerivation decl_use
lepton_hierarchy_geometric in IndisputableMonolith.Masses.MassHierarchy decl_use
r_electron in IndisputableMonolith.Masses.MassHierarchy decl_use
r_muon in IndisputableMonolith.Masses.MassHierarchy decl_use
r_tau in IndisputableMonolith.Masses.MassHierarchy decl_use
fermionRung in IndisputableMonolith.Masses.SMVerification decl_use
muon_rung_minus_electron_rung in IndisputableMonolith.Masses.SMVerification decl_use
tauon_rung_minus_electron_rung in IndisputableMonolith.Masses.SMVerification decl_use

Lean names referenced from this declaration's body.