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)
109theorem faceVertexCount_D3 : faceVertexCount 3 = 4 := by native_decide
proof body
Term-mode proof.
110
111/-- In D=3, there are 6 faces. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
-
D3_has_2D_faces
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
discreteMeasure_eq_4
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
faceVertexCount
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use