theorem proved term proof

`connection_cert`

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

formal statement (Lean)

 133theorem connection_cert : ConnectionCert where
 134  torsion_free := christoffel_symmetric

Term-mode proof.

 135  flat_vanish := flat_christoffel_vanish
 136
 137end Connection
 138end Gravity
 139end IndisputableMonolith

Lean names referenced from this declaration's body.

christoffel_symmetric in IndisputableMonolith.Gravity.Connection decl_use
ConnectionCert in IndisputableMonolith.Gravity.Connection decl_use
flat_christoffel_vanish in IndisputableMonolith.Gravity.Connection decl_use
christoffel_symmetric in IndisputableMonolith.Relativity.Geometry.Curvature decl_use