def
definition
particlePhysicsDepthCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.ParticlePhysicsDepthFromRS on GitHub at line 39.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
36 six_quarks : quarkFlavors = 6
37 six_leptons : leptonFlavors = 6
38
39def particlePhysicsDepthCert : ParticlePhysicsDepthCert where
40 five_detectors := detectionMethodCount
41 six_quarks := quarkFlavors_eq_cubeFaces
42 six_leptons := leptonFlavors_eq_cubeFaces
43
44end IndisputableMonolith.Physics.ParticlePhysicsDepthFromRS