def definition def or abbrev

`diffGeoCert`

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

formal statement (Lean)

  38def diffGeoCert : DiffGeoCert where
  39  five_structures := diffGeoStructureCount

Definition body.

  40  spacetime_4 := rsSpacetimeDim_eq_4
  41
  42end IndisputableMonolith.Mathematics.DifferentialGeometryFromRS

Lean names referenced from this declaration's body.

DiffGeoCert in IndisputableMonolith.Mathematics.DifferentialGeometryFromRS decl_use
diffGeoStructureCount in IndisputableMonolith.Mathematics.DifferentialGeometryFromRS decl_use
rsSpacetimeDim_eq_4 in IndisputableMonolith.Mathematics.DifferentialGeometryFromRS decl_use