pith. machine review for the scientific record. sign in
structure definition def or abbrev

HilbertVariationCert

show as:
view Lean formalization →

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)

 120structure HilbertVariationCert where
 121  flat_ok : hilbert_variation_holds minkowski minkowski_inverse
 122    (fun _ _ _ => 0) (fun _ _ _ _ => 0)
 123  eh_flat : ∀ det_g kappa : ℝ, kappa ≠ 0 → eh_lagrangian_density 0 det_g kappa = 0
 124  einstein_symmetric : ∀ met ginv gamma dgamma,
 125    (∀ mu nu, ricci_tensor gamma dgamma mu nu = ricci_tensor gamma dgamma nu mu) →
 126    ∀ mu nu, einstein_tensor met ginv gamma dgamma mu nu =
 127             einstein_tensor met ginv gamma dgamma nu mu
 128  einstein_flat : ∀ mu nu, einstein_tensor minkowski minkowski_inverse
 129    (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0
 130

used by (1)

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

depends on (17)

Lean names referenced from this declaration's body.