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)
26def Dspatial : ℕ := 3
used by (8)
From the project-wide theorem graph. These declarations reference this one in their body.
-
CardinalitySpectrumCert
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use
-
cubeFaces
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use
-
cubeFaces_eq
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use
-
eightTick
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use
-
eightTick_eq
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use
-
gap45_eq
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use
-
three_is_Dspatial
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use
-
twelve_is_D_4
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use