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)
41def G2 : ℕ := 2 -- binary face
used by (16)
From the project-wide theorem graph. These declarations reference this one in their body.
-
eight_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
four_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
-
seven_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
seventy_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
six_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
sixteen_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
ten_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
-
twoFiftySix_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
twoSixteen_decomp
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use