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)

  35inductive Lepton where
  36  | electron | muon | tau | nuE | nuMu | nuTau
  37  deriving DecidableEq, Repr, BEq, Fintype
  38

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_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
sectorOf in IndisputableMonolith.Masses.RungConstructor.Basic decl_use

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.

tau in IndisputableMonolith.Masses.Anchor decl_use
Lepton in IndisputableMonolith.Physics.AnomalousMoments decl_use