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)
42noncomputable def covariant_deriv_vector (_g : MetricTensor)
43 (_V : VectorField) (_μ : Fin 4) : VectorField := fun _ _ _ => 0
proof body
Definition body.
44
45/-- Covariant derivative of a covector field; collapses to zero. -/
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
MetricTensor
in IndisputableMonolith.Foundation.Hamiltonian
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
MetricTensor
in IndisputableMonolith.Gravity.Connection
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
MetricTensor
in IndisputableMonolith.Meta.Homogenization
decl_use
-
VectorField
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
MetricTensor
in IndisputableMonolith.Relativity.Geometry.Metric
decl_use
-
VectorField
in IndisputableMonolith.Relativity.Geometry.Tensor
decl_use