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)
106theorem r0_Lepton_eq : r0 .Lepton = 62 := by
proof body
Term-mode proof.
107 simp only [r0, W, wallpaper_groups]
108 norm_num
109
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (8)
Lean names referenced from this declaration's body.
-
wallpaper_groups
in IndisputableMonolith.Constants.AlphaDerivation
decl_use
-
wallpaper_groups
in IndisputableMonolith.Constants.AlphaHigherOrder
decl_use
-
Lepton
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
r0
in IndisputableMonolith.Masses.Anchor
decl_use
-
W
in IndisputableMonolith.Masses.Anchor
decl_use
-
Lepton
in IndisputableMonolith.Physics.AnomalousMoments
decl_use
-
W
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
W
in IndisputableMonolith.Physics.MassTopology
decl_use