theorem proved term proof

`euler_identity_Q3`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 212theorem euler_identity_Q3 :
 213    cube_vertices' 3 + cube_faces' 3 - cube_body = cube_edges' 3 + 1 := by

Term-mode proof.

 214  native_decide
 215
 216/-- Therefore 13 has three equivalent natural-invariant interpretations. -/

From the project-wide theorem graph. These declarations reference this one in their body.

thirteen_natural_interpretations in IndisputableMonolith.Masses.StepValueEnumeration decl_use

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
cube_body in IndisputableMonolith.Masses.SectorDependentTorsion decl_use
cube_edges' in IndisputableMonolith.Masses.SectorDependentTorsion decl_use
cube_faces' in IndisputableMonolith.Masses.SectorDependentTorsion decl_use
cube_vertices' in IndisputableMonolith.Masses.SectorDependentTorsion decl_use