def definition def or abbrev

`curvatureFactsStub`

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

formal statement (Lean)

  30noncomputable def curvatureFactsStub : CurvatureExpansionFacts where
  31  riemann_expansion := by intro g₀ h x ρ σ μ ν; norm_num

proof body

Definition body.

  32  ricci_expansion := by intro g₀ h x μ ν; norm_num
  33  ricci_scalar_expansion := by intro g₀ h x; norm_num
  34
  35instance : CurvatureExpansionFacts := curvatureFactsStub
  36