No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
166def leptonCerts : List ResidueCert := [cert_e, cert_mu, cert_tau]
proof body
Definition body.
167
168/-- The quark certificates show more variation due to Quarter-Ladder effects. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
allCerts
in IndisputableMonolith.RSBridge.ResidueData
decl_use
depends on (5)
Lean names referenced from this declaration's body.
-
ResidueCert
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
ResidueCert
in IndisputableMonolith.RSBridge.Anchor
decl_use
-
cert_e
in IndisputableMonolith.RSBridge.ResidueData
decl_use
-
cert_mu
in IndisputableMonolith.RSBridge.ResidueData
decl_use
-
cert_tau
in IndisputableMonolith.RSBridge.ResidueData
decl_use