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)
42def G3 : ℕ := 3 -- spatial dim
used by (11)
From the project-wide theorem graph. These declarations reference this one in their body.
-
fifteen_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
fortyfive_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
generators_minimal
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
primorial_product
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
RecognitionGeneratorsCert
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
second_primorial
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
six_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
third_primorial
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
threeSixty_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
twelve_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
twoSixteen_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
dim
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use