inductive definition def or abbrev

`Lepton`

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

formal statement (Lean)

  19inductive Lepton | e | mu | tau
  20deriving DecidableEq, Repr, Inhabited
  21

used by (40)

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

CubeFaceUniversalityCert in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
fermion_antifermion_total in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
Lepton in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
lepton_has_6 in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
quark_lepton_sum in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
B_pow in IndisputableMonolith.Masses.Anchor decl_use
B_pow_Lepton_eq in IndisputableMonolith.Masses.Anchor decl_use
r0 in IndisputableMonolith.Masses.Anchor decl_use
r0_Lepton_eq in IndisputableMonolith.Masses.Anchor decl_use
Sector in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
B_pow_alt in IndisputableMonolith.Masses.AnchorDerivation decl_use
r0_alt in IndisputableMonolith.Masses.AnchorDerivation decl_use
predict_mass in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung_sdgt in IndisputableMonolith.Masses.AnchorPolicy decl_use
minimal_complete_coefficients in IndisputableMonolith.Masses.BaselineDerivation decl_use
neutrino_baseline_eq in IndisputableMonolith.Masses.BaselineDerivation decl_use
ChargedLeptonMassScoreCardCert in IndisputableMonolith.Masses.ChargedLeptonMassScoreCard decl_use
row_electron_rel in IndisputableMonolith.Masses.ChargedLeptonMassScoreCard decl_use
row_muon_rel in IndisputableMonolith.Masses.ChargedLeptonMassScoreCard decl_use
row_tau_rel in IndisputableMonolith.Masses.ChargedLeptonMassScoreCard decl_use
tau_muon_ratio in IndisputableMonolith.Masses.LeptonMassLadder decl_use
SchemeReconciliationCert in IndisputableMonolith.Masses.QuarkSchemeReconciliation decl_use
QuarkScoreCardCert in IndisputableMonolith.Masses.QuarkScoreCard decl_use
row_electron_pct in IndisputableMonolith.Masses.QuarkScoreCard decl_use
row_muon_pct in IndisputableMonolith.Masses.QuarkScoreCard decl_use
row_quark_preds_pos in IndisputableMonolith.Masses.QuarkScoreCard decl_use
row_tau_pct in IndisputableMonolith.Masses.QuarkScoreCard decl_use
Sector in IndisputableMonolith.Masses.RungConstructor.Basic decl_use

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.

mu in IndisputableMonolith.Cost.Ndim.Projector decl_use
Lepton in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
tau in IndisputableMonolith.Masses.Anchor decl_use